proposition: Lemma seq_singl_wmax r a b (MAX: wmax_elt r b) : singl_rel a b⨾ r ⊆ singl_rel a b.
proof: Proof. unfold singl_rel, seq; red; ins; desf; eauto. apply MAX in H0; desf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid