proposition: Lemma eq_dep_same_inv : forall (A : Type) (P : A -> Type) (p : A) (x y : P p), eq_dep x y -> x = y.
proof: Proof. Proof using. introv R. inversion R. apply eq_dep_nd_same_inv. apply~ eq_dep_nd_of_eq_dep. Qed.
imports: TLC(LibTactics LibAxioms)