proposition: Lemma eq_existT_same_inv : forall (A : Type) (P : A -> Type) (p : A) (x y : P p), existT P p x = existT P p y -> x = y.
proof: Proof. Proof using. intros. apply eq_dep_nd_same_inv. apply~ eq_existT_inv. Qed.
imports: TLC(LibTactics LibAxioms)