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