proposition: Lemma eq_dep_trans : forall (A : Type) (P : A -> Type) (p q r : A) (y : P q) (x : P p) (z : P r), eq_dep x y -> eq_dep y z -> eq_dep x z.
proof: Proof. Proof using. introv E F. destruct~ E. Qed.
imports: TLC(LibTactics LibAxioms)