we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc1_props.v b/helm/coq-contribs/LAMBDA-TYPES/pc1_props.v
deleted file mode 100644 (file)
index 840a79c..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pc1_props.v
+++ /dev/null
@@ -1,25 +0,0 @@
-Require pr1_confluence.
-Require pc1_defs. 
-
-(*#* #stop file *)
-
-   Section pc1_trans. (******************************************************)
-
-      Theorem pc1_t: (t2,t1:?) (pc1 t1 t2) ->
-                     (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
-      Intros; Repeat Pc1Unfold; Pr1Confluence; XEAuto.
-      Qed.
-
-      Theorem pc1_pr0_u2: (t0,t1:?) (pr0 t0 t1) ->
-                          (t2:?) (pc1 t0 t2) -> (pc1 t1 t2).
-      Intros; Apply (pc1_t t0); XAuto.
-      Qed.
-
-      Theorem pc1_tail: (u1,u2:?) (pc1 u1 u2) -> (t1,t2:?) (pc1 t1 t2) ->
-                        (k:?) (pc1 (TTail k u1 t1) (TTail k u2 t2)).
-      Intros; EApply pc1_t; [ EApply pc1_tail_1 | EApply pc1_tail_2 ]; XAuto.
-      Qed.
-
-   End pc1_trans.
-
-      Hints Resolve pc1_t pc1_tail : ltlc.