proposition: Lemma eq_dep_nd_same_inv : forall (A : Type) (P : A -> Type) (p : A) (x y : P p), eq_dep_nd x y -> x = y.
proof: Proof. Proof using. introv H. inversions H. rewrite~ eq_rect_refl_eq. Qed.
imports: TLC(LibTactics LibAxioms)