proposition: Lemma eq_existT_inv : forall (A : Type) (P : A -> Type) (p q : A) (x : P p) (y : P q), existT P p x = existT P q y -> eq_dep_nd x y.
proof: Proof. Proof using. introv E. dependent rewrite E. simpl. apply eq_dep_nd_refl. Qed.
imports: TLC(LibTactics LibAxioms)