fact: Definition eq_ex2_nondep {A : Prop} {B C : Prop} (u v : @ex2 A (fun _ => B) (fun _ => C)) (p : ex_proj1 u = ex_proj1 v) (q : ex_proj2 u = ex_proj2 v) (r : ex_proj3 u = ex_proj3 v) : u = v := @eq_ex2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
imports: Notations Ltac