proposition: Lemma inclusion_ct_seq_eqv_l A dom (r : relation A) : (⦗dom⦘ ⨾ r)⁺ ⊆ ⦗dom⦘ ⨾ r⁺.
proof: Proof. by rewrite ct_begin, seqA, inclusion_seq_eqv_l with (r:=r), <- ct_begin. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets