Section Dependent_equality.

Variable U:Type.
Variable P:U->Type.

Inductive eq_depT [p:U;x:(P p)] : (q:U)(P q)->Prop :=
   eq_depT_intro : (eq_depT p x p x).

End Dependent_equality.