proposition: Lemma collect_rel_compose (f : A -> B) (g : B -> C) r : (g ∘ f) ↑ r ≡ g ↑ (f ↑ r).
proof: Proof. unfold compose. repeat autounfold with unfolderDb. ins; splits; ins; splits; desf; eauto 10. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets