we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v
deleted file mode 100644 (file)
index 22b4fce..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v
+++ /dev/null
@@ -1,50 +0,0 @@
-(*#* #stop file *)
-
-Require Export pr0_defs.
-Require Export pr1_defs.
-
-      Definition pc1 := [t1,t2:?] (EX t | (pr1 t1 t) & (pr1 t2 t)). 
-
-      Hints Unfold pc1 : ltlc.
-
-      Tactic Definition Pc1Unfold :=
-         Match Context With
-            [ H: (pc1 ?2 ?3) |- ? ] -> Unfold pc1 in H; XDecompose H.
-
-   Section pc1_props. (******************************************************)
-
-      Theorem pc1_pr0_r: (t1,t2:?) (pr0 t1 t2) -> (pc1 t1 t2).
-      XEAuto.
-      Qed.
-
-      Theorem pc1_pr0_x: (t1,t2:?) (pr0 t2 t1) -> (pc1 t1 t2).
-      XEAuto.
-      Qed.
-
-      Theorem pc1_pr0_u: (t2,t1:?) (pr0 t1 t2) ->
-                         (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
-      Intros; Pc1Unfold; XEAuto.
-      Qed.
-      
-      Theorem pc1_refl: (t:?) (pc1 t t).
-      XEAuto.
-      Qed.
-
-      Theorem pc1_s: (t2,t1:?) (pc1 t1 t2) -> (pc1 t2 t1).
-      Intros; Pc1Unfold; XEAuto.
-      Qed.
-
-      Theorem pc1_tail_1: (u1,u2:?) (pc1 u1 u2) ->
-                          (t:?; k:?) (pc1 (TTail k u1 t) (TTail k u2 t)).
-      Intros; Pc1Unfold; XEAuto.
-      Qed.
-
-      Theorem pc1_tail_2: (t1,t2:?) (pc1 t1 t2) ->
-                          (u:?; k:?) (pc1 (TTail k u t1) (TTail k u t2)).
-      Intros; Pc1Unfold; XEAuto.
-      Qed.
-
-   End pc1_props.
-
-      Hints Resolve pc1_refl pc1_pr0_u pc1_pr0_r pc1_pr0_x pc1_s
-                    pc1_tail_1 pc1_tail_2 : ltlc.