proposition: Lemma simplification_existT1 A (P : A -> Type) B (p q : A) (x : P p) (y : P q) : (p = q -> conditional_eq (existT P p x) (existT P q y) -> B) -> (existT P p x = existT P q y -> B).
proof: Proof. injection 2. auto. Defined.
imports: JMeq Coq.Program.Tactics Eqdep