∀ {α : Type u_1} (c : Order.Frame α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α)
  (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (himp : α → α → α)
  (eq_himp : himp = HImp.himp) (compl : α → α) (eq_compl : compl = Compl.compl) (a b : α), Lattice.inf a b ≤ a