we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/csub0_props.v b/helm/coq-contribs/LAMBDA-TYPES/csub0_props.v
deleted file mode 100644 (file)
index 04c4edd..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/csub0_props.v
+++ /dev/null
@@ -1,67 +0,0 @@
-(*#* #stop file *)
-
-Require pc3_props.
-Require csub0_defs.   
-
-   Section csub0_pc3. (*****************************************************)
-
-      Theorem csub0_pr2: (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
-                         (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2).
-      Intros until 1; XElim H; Intros.
-(* case 1: pr2_free *)
-      XAuto.
-(* case 2: pr2_delta *)
-      CSub0Drop; XEAuto.
-      Qed.
-
-      Hints Resolve csub0_pr2.
-
-      Opaque pc3.
-
-      Theorem csub0_pc3: (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) ->
-                         (c2:?) (csub0 g c1 c2) -> (pc3 c2 t1 t2).
-      Intros until 1; XElimUsing pc3_ind_left H; XEAuto.
-      Qed.
-
-   End csub0_pc3.
-
-      Hints Resolve csub0_pc3 : ltlc.
-   
-   Section csub0_ty0. (*****************************************************)
-
-      Theorem csub0_ty0: (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
-                         (c2:?) (wf0 g c2) -> (csub0 g c1 c2) ->
-                         (ty0 g c2 t1 t2).
-      Intros until 1; XElim H; Intros.
-(* case 1: ty0_conv *)
-      EApply ty0_conv; XEAuto.
-(* case 2: ty0_sort *)
-      XEAuto.
-(* case 3: ty0_abbr *)
-      CSub0Drop; EApply ty0_abbr; XEAuto.
-(* case 4: ty0_abst *)
-      CSub0Drop; [ EApply ty0_abst | EApply ty0_abbr ]; XEAuto.
-(* case 5: ty0_bind *)
-      EApply ty0_bind; XEAuto.
-(* case 6: ty0_appl *)
-      EApply ty0_appl; XEAuto.
-(* case 7: ty0_cast *)
-      EApply ty0_cast; XAuto.
-      Qed.
-
-      Theorem csub0_ty0_ld: (g:?; c:?; u,v:?) (ty0 g c u v) -> (t1,t2:?)
-                            (ty0 g (CTail c (Bind Abst) v) t1 t2) ->
-                            (ty0 g (CTail c (Bind Abbr) u) t1 t2).
-      Intros; EApply csub0_ty0; XEAuto.
-      Qed.
-
-   End csub0_ty0.
-
-      Hints Resolve csub0_ty0 csub0_ty0_ld : ltlc.
-
-      Tactic Definition CSub0Ty0 :=
-         Match Context With
-            [ _: (ty0 ?1 ?2 ?4 ?); _: (ty0 ?1 ?2 ?3 ?7); _: (pc3 ?2 ?4 ?7);
-              H: (ty0 ?1 (CTail ?2 (Bind Abst) ?4) ?5 ?6) |- ? ] ->
-               LApply (csub0_ty0_ld ?1 ?2 ?3 ?4); [ Intros H_x | EApply ty0_conv; XEAuto ];
-               LApply (H_x ?5 ?6); [ Clear H_x H; Intros | XAuto ].