X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fcpr0_defs.v;fp=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fcpr0_defs.v;h=ce6faccba461419f3e6edf7da5e436204c9cec63;hb=1b21075e987872a2e3103203b4e67c939e4a9f6a;hp=0000000000000000000000000000000000000000;hpb=ea6b99ed26a954a578e3c88909479dcf9cab7345;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v
new file mode 100644
index 000000000..ce6faccba
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v
@@ -0,0 +1,11 @@
+(*#* #stop file *)
+
+Require Export contexts_defs.
+Require Export pr0_defs.
+
+      Inductive cpr0 : C -> C -> Prop :=
+         | cpr0_refl : (c:?) (cpr0 c c)
+         | cpr0_cont : (c1,c2:?) (cpr0 c1 c2) -> (u1,u2:?) (pr0 u1 u2) ->
+                       (k:?) (cpr0 (CTail c1 k u1) (CTail c2 k u2)).
+
+      Hint cpr0 : ltlc := Constructors cpr0.