{α : Type u_5} →
  {P : Sort u} →
    {toLattice : Lattice α} →
      {toSupSet : SupSet α} →
        {toInfSet : InfSet α} →
          {le_csSup : ∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup s} →
            {csSup_le : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ upperBounds s → sSup s ≤ a} →
              {csInf_le : ∀ (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ a} →
                {le_csInf : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s} →
                  {toLattice' : Lattice α} →
                    {toSupSet' : SupSet α} →
                      {toInfSet' : InfSet α} →
                        {le_csSup' : ∀ (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup s} →
                          {csSup_le' : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ upperBounds s → sSup s ≤ a} →
                            {csInf_le' : ∀ (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ a} →
                              {le_csInf' : ∀ (s : Set α) (a : α), s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s} →
                                { toLattice := toLattice, toSupSet := toSupSet, toInfSet := toInfSet,
                                      le_csSup := le_csSup, csSup_le := csSup_le, csInf_le := csInf_le,
                                      le_csInf := le_csInf } =
                                    { toLattice := toLattice', toSupSet := toSupSet', toInfSet := toInfSet',
                                      le_csSup := le_csSup', csSup_le := csSup_le', csInf_le := csInf_le',
                                      le_csInf := le_csInf' } →
                                  (toLattice ≍ toLattice' → toSupSet ≍ toSupSet' → toInfSet ≍ toInfSet' → P) → P