{X : Type u} →
  {inst : Lattice X} →
    {P : Sort u_1} →
      {IsMaximal : X → X → Prop} →
        {lt_of_isMaximal : ∀ {x y : X}, IsMaximal x y → x < y} →
          {sup_eq_of_isMaximal : ∀ {x y z : X}, IsMaximal x z → IsMaximal y z → x ≠ y → x ⊔ y = z} →
            {isMaximal_inf_left_of_isMaximal_sup :
                ∀ {x y : X}, IsMaximal x (x ⊔ y) → IsMaximal y (x ⊔ y) → IsMaximal (x ⊓ y) x} →
              {Iso : X × X → X × X → Prop} →
                {iso_symm : ∀ {x y : X × X}, Iso x y → Iso y x} →
                  {iso_trans : ∀ {x y z : X × X}, Iso x y → Iso y z → Iso x z} →
                    {second_iso : ∀ {x y : X}, IsMaximal x (x ⊔ y) → Iso (x, x ⊔ y) (x ⊓ y, y)} →
                      {IsMaximal' : X → X → Prop} →
                        {lt_of_isMaximal' : ∀ {x y : X}, IsMaximal' x y → x < y} →
                          {sup_eq_of_isMaximal' : ∀ {x y z : X}, IsMaximal' x z → IsMaximal' y z → x ≠ y → x ⊔ y = z} →
                            {isMaximal_inf_left_of_isMaximal_sup' :
                                ∀ {x y : X}, IsMaximal' x (x ⊔ y) → IsMaximal' y (x ⊔ y) → IsMaximal' (x ⊓ y) x} →
                              {Iso' : X × X → X × X → Prop} →
                                {iso_symm' : ∀ {x y : X × X}, Iso' x y → Iso' y x} →
                                  {iso_trans' : ∀ {x y z : X × X}, Iso' x y → Iso' y z → Iso' x z} →
                                    {second_iso' : ∀ {x y : X}, IsMaximal' x (x ⊔ y) → Iso' (x, x ⊔ y) (x ⊓ y, y)} →
                                      { IsMaximal := IsMaximal, lt_of_isMaximal := lt_of_isMaximal,
                                            sup_eq_of_isMaximal := sup_eq_of_isMaximal,
                                            isMaximal_inf_left_of_isMaximal_sup := isMaximal_inf_left_of_isMaximal_sup,
                                            Iso := Iso, iso_symm := iso_symm, iso_trans := iso_trans,
                                            second_iso := second_iso } =
                                          { IsMaximal := IsMaximal', lt_of_isMaximal := lt_of_isMaximal',
                                            sup_eq_of_isMaximal := sup_eq_of_isMaximal',
                                            isMaximal_inf_left_of_isMaximal_sup := isMaximal_inf_left_of_isMaximal_sup',
                                            Iso := Iso', iso_symm := iso_symm', iso_trans := iso_trans',
                                            second_iso := second_iso' } →
                                        (IsMaximal ≍ IsMaximal' → Iso ≍ Iso' → P) → P