we restored the scripts of \lambda\delta version 1

[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
deleted file mode 100644 (file)
index ed05b0e..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pr1_defs.v
+++ /dev/null
@@ -1,34 +0,0 @@
-(*#* #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 until 1; XElim H; XEAuto.
-      Qed.
-
-      Theorem pr1_tail_1: (u1,u2:?) (pr1 u1 u2) -> 
-                          (t:?; k:?) (pr1 (TTail k u1 t) (TTail k u2 t)).
-      Intros; XElim H; XEAuto.
-      Qed.
-
-      Theorem pr1_tail_2: (t1,t2:?) (pr1 t1 t2) ->
-                          (u:?; k:?) (pr1 (TTail k u t1) (TTail k u t2)).
-      Intros; XElim H; XEAuto.
-      Qed.
-
-   End pr1_props.
-
-      Hints Resolve pr1_pr0 pr1_t pr1_tail_1 pr1_tail_2 : ltlc.