proposition: Lemma seq_min r r' b (MAX: min_elt r b) (DOM: forall x y, r' x y -> x = b) : r ⨾ r' ≡ ∅₂.
proof: Proof. unfold seq; split; red; ins; desf. apply DOM in H0; desf; eauto. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid