λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
notation < "x \sub \neq" non associative with precedence 91 for @{'bsss $x}.
λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
notation < "x \sub \neq" non associative with precedence 91 for @{'bsss $x}.