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