proposition: Lemma eq_existT_same_eq : 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. extens. iff M. { apply eq_dep_nd_same_inv. apply~ eq_existT_inv. } { subst*. } Qed.
imports: TLC(LibTactics LibAxioms)