{α : Type u_4} →
  {P : Sort u} →
    {toLattice : Lattice α} →
      {toOrderTop : OrderTop α} →
        {toHImp : HImp α} →
          {le_himp_iff : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c} →
            {toLattice' : Lattice α} →
              {toOrderTop' : OrderTop α} →
                {toHImp' : HImp α} →
                  {le_himp_iff' : ∀ (a b c : α), a ≤ b ⇨ c ↔ a ⊓ b ≤ c} →
                    { toLattice := toLattice, toOrderTop := toOrderTop, toHImp := toHImp, le_himp_iff := le_himp_iff } =
                        { toLattice := toLattice', toOrderTop := toOrderTop', toHImp := toHImp',
                          le_himp_iff := le_himp_iff' } →
                      (toLattice ≍ toLattice' → toOrderTop ≍ toOrderTop' → toHImp ≍ toHImp' → P) → P