proposition: Lemma map_map_exchange: forall A F G B (f1 : F -> B) (f2 : A -> F) (g1 : G -> B) (g2 : A -> G) e, (forall (d : A), f1 (f2 d) = g1 (g2 d)) -> map f1 (map f2 e) = map g1 (map g2 e).
proof: Proof. induction e; intros; try match goal with o: option _ |- _ => destruct o end; simpl; eauto with f_equal. Qed.
imports: List Dblib(DblibTactics DeBruijn)