proposition: Lemma collect_rel_singl f x y : f ↑ singl_rel x y ≡ singl_rel (f x) (f y).
proof: Proof. u; eauto 8. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets