proposition: Lemma seq_eqv_max_t r : ⦗max_elt r⦘ ⨾ r⁺ ≡ (∅₂).
proof: Proof. rewrite ct_begin; seq_rewrite seq_eqv_max; basic_solver. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid