proposition: Lemma transp_seq_eqv_max_t r : (r⁻¹)⁺ ⨾ ⦗max_elt r⦘ ≡ (∅₂).
proof: Proof. rewrite ct_end, !seqA; seq_rewrite transp_seq_eqv_max; basic_solver. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite Arith Setoid