proposition: Lemma seq_eqv_min_transp_t r : ⦗min_elt r⦘ ⨾ (r⁻¹)⁺ ≡ ∅₂.
proof: Proof. rewrite ct_begin; seq_rewrite seq_eqv_min_transp; basic_solver. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnMaxElt Arith Setoid