]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportcsczfc/csc_zfc/csc_eqdep.v
projects / helm.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
ocaml 3.09 transition
[helm.git] / helm / EXPORT / exportcsczfc / csc_zfc / csc_eqdep.v
1 Section Dependent_equality.
2
3 Variable U:Type.
4 Variable P:U->Type.
5
6 Inductive eq_depT [p:U;x:(P p)] : (q:U)(P q)->Prop :=
7    eq_depT_intro : (eq_depT p x p x).
8
9 End Dependent_equality.
Unnamed repository; edit this file 'description' to name the repository.