proposition: Lemma map_rel_compose (f : A -> B) (g : B -> C) r : (g ∘ f) ↓ r ≡ f ↓ (g ↓ 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