proposition: Lemma simplification_existT1 : forall {A} {P : A -> Type} {B} (p q : A) (x : P p) (y : P q), (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B).
proof: Proof. intros. refine (X _ H). change (projT1 (existT P p x) = projT1 (existT P q y)). now destruct H. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.CoreTactics Equations.Signature Equations.Prop.Logic Equations.Prop.Classes Equations.Prop.EqDec