proposition: Lemma simplification_existT2 A (P : A -> Type) B (p : A) (x y : P p) : (x = y -> B) -> (conditional_eq (existT P p x) (existT P p y) -> B).
proof: Proof. intros H E. apply H. apply inj_pair2. assumption. Defined.
imports: JMeq Coq.Program.Tactics Eqdep