proposition: Lemma map_insert_map: forall A (f g h : A -> A) x (a : A) e, (forall a, f (g a) = g (h a)) -> map f (insert x a (map g e)) = insert x (f a) (map g (map h e)).
proof: Proof. intros. rewrite map_insert. f_equal. eapply map_map_exchange. eauto. Qed.
imports: List Dblib(DblibTactics DeBruijn)