proposition: Lemma set_collect_compose (f : A -> B) (g : B -> C) s : (g ∘ f) ↑₁ s ≡₁ g ↑₁ (f ↑₁ s) .
proof: Proof. unfold compose. repeat autounfold with unfolderDb. ins; splits; ins; splits; desf; eauto. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms