{X : Type u} →
  [inst : Lattice X] →
    (IsMaximal : X → X → Prop) →
      (∀ {x y : X}, IsMaximal x y → x < y) →
        (∀ {x y z : X}, IsMaximal x z → IsMaximal y z → x ≠ y → x ⊔ y = z) →
          (∀ {x y : X}, IsMaximal x (x ⊔ y) → IsMaximal y (x ⊔ y) → IsMaximal (x ⊓ y) x) →
            (Iso : X × X → X × X → Prop) →
              (∀ {x y : X × X}, Iso x y → Iso y x) →
                (∀ {x y z : X × X}, Iso x y → Iso y z → Iso x z) →
                  (∀ {x y : X}, IsMaximal x (x ⊔ y) → Iso (x, x ⊔ y) (x ⊓ y, y)) → JordanHolderLattice X