proposition: Lemma eq_exist_curried {A : Type} {P : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1} (p : u1 = v1) (q : rew p in u2 = v2) : exist P u1 u2 = exist P v1 v2.
proof: Proof. apply eq_sig_uncurried; exists p; exact q. Defined.
imports: Notations Ltac Datatypes Logic