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