proposition: Lemma f_equal_dep2 {A A' B B'} (f : A -> A') (g : forall a:A, B a -> B' (f a)) {x1 x2 : A} {y1 : B x1} {y2 : B x2} (H : x1 = x2) : rew H in y1 = y2 -> rew f_equal f H in g x1 y1 = g x2 y2.
proof: Proof. destruct H, 1. reflexivity. Defined.
imports: Notations Ltac