proposition: Lemma seq_singl_wmax_t r a b (MAX: wmax_elt r b) : singl_rel a b⨾ r ⁺ ⊆ singl_rel a b.
proof: Proof. eauto using seq_singl_wmax with hahn. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid