proposition: Lemma seq_singl_max r a b (MAX: max_elt r b) : singl_rel a b ⨾ r ≡ ∅₂.
proof: Proof. unfold singl_rel, seq; split; red; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid