{α : Type u_2} →
  {inst : Lattice α} →
    {P : Sort u} →
      {toSetoid : Setoid α} →
        {inf : ∀ {w x y z : α}, toSetoid w x → toSetoid y z → toSetoid (w ⊓ y) (x ⊓ z)} →
          {sup : ∀ {w x y z : α}, toSetoid w x → toSetoid y z → toSetoid (w ⊔ y) (x ⊔ z)} →
            {toSetoid' : Setoid α} →
              {inf' : ∀ {w x y z : α}, toSetoid' w x → toSetoid' y z → toSetoid' (w ⊓ y) (x ⊓ z)} →
                {sup' : ∀ {w x y z : α}, toSetoid' w x → toSetoid' y z → toSetoid' (w ⊔ y) (x ⊔ z)} →
                  { toSetoid := toSetoid, inf := inf, sup := sup } =
                      { toSetoid := toSetoid', inf := inf', sup := sup' } →
                    (toSetoid ≍ toSetoid' → P) → P