proposition: Lemma map_subst_map {A B} {P:A->Type} {Q:B->Type} (f:A->B) (g : forall x, P x -> Q (f x)) {x y} (H:x=y) (z:P x) : rew f_equal f H in g x z = g y (rew H in z).
proof: Proof. destruct H. reflexivity. Defined.
imports: Notations Ltac