{α : Type u_6} →
  {β : Type u_7} →
    [inst : BiheytingAlgebra α] →
      [inst_1 : BiheytingAlgebra β] →
        {motive : BiheytingHom α β → Sort u} →
          ((toLatticeHom : LatticeHom α β) →
              (map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b) →
                (map_sdiff' : ∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b) →
                  motive { toLatticeHom := toLatticeHom, map_himp' := map_himp', map_sdiff' := map_sdiff' }) →
            (t : BiheytingHom α β) → motive t