proposition: Lemma eq_dep_of_eq_dep_nd : forall (A : Type) (P : A -> Type) (p q : A) (x : P p) (y : P q), eq_dep_nd x y -> eq_dep x y.
proof: Proof. Proof using. introv E. destruct E as (h,H). destruct h using eq_induction. subst~. constructor. Qed.
imports: TLC(LibTactics LibAxioms)