fact: Definition path_ex' {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1) (p : u1 = v1) (q : eq_rect _ _ u2 _ p = v2) : ex_intro P u1 u2 = ex_intro P v1 v2 := path_ex_uncurried' P (ex_intro _ p q).
imports: Fiat.Common.Equality