proposition: Lemma inclusion_ct_seq_eqv_r A dom (r : relation A) : (r ⨾ ⦗dom⦘)⁺ ⊆ r⁺ ⨾ ⦗dom⦘.
proof: Proof. by rewrite ct_end, inclusion_seq_eqv_r at 1; rewrite <- seqA, <- ct_end. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets