fact: Definition eq_ex_intro2_hprop_nondep {A : Type} {P : A -> Prop} {Q : Prop} (Q_hprop : forall (p q : Q), p = q) {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 v3 : Q} (p : ex_intro _ u1 u2 = ex_intro _ v1 v2) : ex_intro2 _ _ u1 u2 u3 = ex_intro2 _ _ v1 v2 v3 := rew [fun v3 => _ = ex_intro2 _ _ _ _ v3] (Q_hprop u3 v3) in f_equal (fun u => match u with ex_intro _ u1 u2 => ex_intro2 _ _ u1 u2 u3 end) p.
imports: Notations Ltac