we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v
deleted file mode 100644 (file)
index 6f5019b..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v
+++ /dev/null
@@ -1,59 +0,0 @@
-Require pr2_confluence.
-Require pr3_defs.
-
-   Section pr3_confluence. (*************************************************)
-
-(*#* #stop theorem *)
-
-(*#* #caption "confluence with single step reduction: strip lemma" *)
-(*#* #cap #cap c, t0, t1, t2, t *)
-
-      Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) ->
-                          (EX t | (pr3 c t1 t) & (pr3 c t2 t)).
-      Intros until 1; XElim H; Intros.
-(* case 1 : pr3_refl *)
-      XEAuto.
-(* case 2 : pr3_sing *)
-      Pr2Confluence.
-      LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
-      XElim H1; Intros; XEAuto.
-      Qed.
-
-(*#* #start theorem *)
-
-(*#* #caption "confluence with itself: Church-Rosser property" *)
-(*#* #cap #cap c, t0, t1, t2, t *)
-
-      Theorem pr3_confluence : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr3 c t0 t2) ->
-                               (EX t | (pr3 c t1 t) & (pr3 c t2 t)).
-
-(*#* #stop file *)
-
-      Intros until 1; XElim H; Intros.
-(* case 1 : pr3_refl *)
-      XEAuto.
-(* case 2 : pr3_sing *)
-      LApply (pr3_strip c t3 t5); [ Clear H2; Intros H2 | XAuto ].
-      LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
-      XElim H; Intros.
-      LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
-      XElim H1; Intros; XEAuto.
-      Qed.
-
-   End pr3_confluence.
-
-      Tactic Definition Pr3Confluence :=
-         Match Context With
-            | [ H1: (pr3 ?1 ?2 ?3); H2: (pr2 ?1 ?2 ?4) |-? ] ->
-               LApply (pr3_strip ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
-               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
-               XElim H1; Intros
-            | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 ?1 ?2 ?4) |-? ] ->
-               LApply (pr3_confluence ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
-               LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
-               XElim H1; Intros
-            | _ -> Pr2Confluence.
-
-(*#* #start file *)
-
-(*#* #single *)