contribution about \lambda-\delta

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v
new file mode 100644 (file)
index 0000000..986b594
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v
@@ -0,0 +1,24 @@
+(*#* #stop file *)
+
+Require Export pr0_defs.
+
+      Inductive pr1 : T -> T -> Prop :=
+         | pr1_r : (t:?) (pr1 t t)
+         | pr1_u : (t2,t1:?) (pr0 t1 t2) -> (t3:?) (pr1 t2 t3) -> (pr1 t1 t3).
+
+      Hint pr1 : ltlc := Constructors pr1.
+
+   Section pr1_props. (******************************************************)
+
+      Theorem pr1_pr0 : (t1,t2:?) (pr0 t1 t2) -> (pr1 t1 t2).
+      XEAuto.
+      Qed.
+
+      Theorem pr1_t : (t2,t1:?) (pr1 t1 t2) ->
+                      (t3:?) (pr1 t2 t3) -> (pr1 t1 t3).
+      Intros t2 t1 H; XElim H; XEAuto.
+      Qed.
+
+   End pr1_props.
+
+      Hints Resolve pr1_pr0 pr1_t : ltlc.