proposition: Lemma collect_rel_crt f r : f ↑ r＊ ⊆ (f ↑ r)＊.
proof: Proof. by rewrite <- !cr_of_ct, <- collect_rel_ct, <- collect_rel_cr. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets