proposition: Lemma seq_singl_wmax_r r a b (MAX: wmax_elt r b) : singl_rel a b⨾ r ^? ≡ singl_rel a b.
proof: Proof. rewrite crE; split; relsf; rewrite seq_singl_wmax; relsf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid