proposition: Theorem eq_trans_map {A B} {x1 x2 x3:A} {y1:B x1} {y2:B x2} {y3:B x3} (H1:x1=x2) (H2:x2=x3) (H1': rew H1 in y1 = y2) (H2': rew H2 in y2 = y3) : rew eq_trans H1 H2 in y1 = y3.
proof: Proof. destruct H2. exact (eq_trans H1' H2'). Defined.
imports: Notations Ltac