proposition: Lemma map_fst_map_first {A B C} (l: list (A * B)) (f: A -> C): map (@fst _ _) (map (first f) l) = map f (map (@fst _ _) l).
proof: Proof. induction l; simpl; congruence. Qed.
imports: Coq.Unicode.Utf8 Coq.Setoids.Setoid Coq.Lists.List