definition apart ≝ λE:excedence.λa,b:E. a ≰ b ∨ b ≰ a.
notation "a # b" non associative with precedence 50 for @{ 'apart $a $b}.
definition apart ≝ λE:excedence.λa,b:E. a ≰ b ∨ b ≰ a.
notation "a # b" non associative with precedence 50 for @{ 'apart $a $b}.