contribution about \lambda-\delta

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / cpr0_defs.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v
new file mode 100644 (file)
index 0000000..ce6facc
--- /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.