proposition: Lemma seq_eq_wmax r b (MAX: wmax_elt r b) : ⦗eq b⦘⨾ r ⊆ ⦗eq b⦘.
proof: Proof. eapply seq_wmax; unfold eqv_rel; ins; desf. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid