{α : Type u_6} →
  {β : Type u_7} →
    {inst : HeytingAlgebra α} →
      {inst_1 : HeytingAlgebra β} →
        {P : Sort u} →
          {toLatticeHom : LatticeHom α β} →
            {map_bot' : toLatticeHom.toFun ⊥ = ⊥} →
              {map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b} →
                {toLatticeHom' : LatticeHom α β} →
                  {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', map_bot' := map_bot'', map_himp' := map_himp'' } →
                        (toLatticeHom ≍ toLatticeHom' → P) → P