proposition: Theorem eq_existT_curried_congr {A P} {u1 v1 : A} {u2 : P u1} {v2 : P v1} {p p' : u1 = v1} {q : rew p in u2 = v2} {q': rew p' in u2 = v2} (r : p = p') : rew [fun H => rew H in u2 = v2] r in q = q' -> (= p; q) = (= p'; q').
proof: Proof. destruct r, 1. reflexivity. Qed.
imports: Notations Ltac Datatypes Logic