proposition: Lemma eq_existT_curried_trans {A P} {u1 v1 w1 : A} {u2 : P u1} {v2 : P v1} {w2 : P w1} (p : u1 = v1) (q : rew p in u2 = v2) (p' : v1 = w1) (q': rew p' in v2 = w2) : eq_trans (= p; q) (= p'; q') = (= eq_trans p p'; eq_trans_map p p' q q').
proof: Proof. destruct p', q'. reflexivity. Defined.
imports: Notations Ltac Datatypes Logic