∀ {α : Type u_6} {β : Type u_7} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β] (toLatticeHom : LatticeHom α β)
  (map_bot' : toLatticeHom.toFun ⊥ = ⊥)
  (map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b)
  (toLatticeHom_1 : LatticeHom α β) (map_bot'_1 : toLatticeHom_1.toFun ⊥ = ⊥)
  (map_himp'_1 : ∀ (a b : α), toLatticeHom_1.toFun (a ⇨ b) = toLatticeHom_1.toFun a ⇨ toLatticeHom_1.toFun b),
  ({ toLatticeHom := toLatticeHom, map_bot' := map_bot', map_himp' := map_himp' } =
      { toLatticeHom := toLatticeHom_1, map_bot' := map_bot'_1, map_himp' := map_himp'_1 }) =
    (toLatticeHom = toLatticeHom_1)