proposition: Lemma seq_eq_max r b (MAX: max_elt r b) : ⦗eq b⦘ ⨾ r ≡ ∅₂.
proof: Proof. eapply seq_max; unfold eqv_rel; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid