proposition: Lemma seq_t_eqv_min r : r⁺ ⨾ ⦗min_elt r⦘ ≡ ∅₂.
proof: Proof. rewrite ct_end, seqA; seq_rewrite seq_eqv_min; basic_solver. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid