X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fcsubst0_defs.v;h=046b1978cf2216204f2b6d1c4db08b28f1c4a642;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=a452fd3f0356cb37476c12af0fc86b5a15415c09;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v
index a452fd3f0..046b1978c 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v
@@ -1,27 +1,26 @@
-(*#* #stop file *)
-
 Require Export contexts_defs.
 Require Export subst0_defs.
 Require Export drop_defs.
 
+(*#* #caption "axioms for strict substitution in contexts",
+   "substituted tail item: second operand", 
+   "substituted tail item: first operand", 
+   "substituted tail item: both operands"
+*)
+(*#* #cap #cap c, c1, c2 #alpha v in W, u in V, u1 in V1, u2 in V2, k in z, r in q *)
+
       Inductive csubst0 : nat -> T -> C -> C -> Prop :=
-         | csubst0_fst  : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) -> (c:?)
-                          (csubst0 (S i) v (CTail c k u) (CTail c k w))
-         | csubst0_snd  : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) ->
+         | csubst0_snd  : (k:?; i:?; v,u1,u2:?) (subst0 (r k i) v u1 u2) -> (c:?)
+                          (csubst0 (S i) v (CTail c k u1) (CTail c k u2))
+         | csubst0_fst  : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) ->
                           (u:?) (csubst0 (S i) v (CTail c1 k u) (CTail c2 k u))
-         | csubst0_both : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) ->
+         | csubst0_both : (k:?; i:?; v,u1,u2:?) (subst0 (r k i) v u1 u2) ->
                           (c1,c2:?) (csubst0 (r k i) v c1 c2) ->
-                          (csubst0 (S i) v (CTail c1 k u) (CTail c2 k w)).
+                          (csubst0 (S i) v (CTail c1 k u1) (CTail c2 k u2)).
 
-      Hint csubst0 : ltlc := Constructors csubst0.
-
-      Inductive fsubst0 [i:nat; v:T; c1:C; t1:T] : C -> T -> Prop :=
-         | fsubst0_t : (t2:?) (subst0 i v t1 t2) -> (fsubst0 i v c1 t1 c1 t2)
-         | fsubst0_c : (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t1)
-         | fsubst0_b : (t2:?) (subst0 i v t1 t2) ->
-                       (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t2).
+(*#* #stop file *)
 
-      Hint fsubst0 : ltlc := Constructors fsubst0.
+      Hint csubst0 : ltlc := Constructors csubst0.
 
    Section csubst0_gen_base. (***********************************************)
 
@@ -39,9 +38,9 @@ Require Export drop_defs.
                                 )).
       Intros until 1; InsertEq H '(S i); InsertEq H '(CTail c1 k u1).
       XCase H; Clear x v y y0; Intros; Inversion H1.
-(* case 1: csubst0_fst *)
+(* case 1: csubst0_snd *)
       Inversion H0; Rewrite H3 in H; Rewrite H5 in H; Rewrite H6 in H; XEAuto.
-(* case 2: csubst0_snd *)
+(* case 2: csubst0_fst *)
       Inversion H0; Rewrite H3 in H; Rewrite H4 in H; Rewrite H5 in H; XEAuto.
 (* case 2: csubst0_both *)
       Inversion H2; Rewrite H5 in H; Rewrite H6 in H; Rewrite H7 in H;
@@ -72,9 +71,9 @@ Require Export drop_defs.
 (* case 2.2: n > 0 *)
       Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros.
       DropGenBase.
-(* case 2.2.1: csubst0_fst *)
+(* case 2.2.1: csubst0_snd *)
       XAuto.
-(* case 2.2.2: csubst0_snd *)
+(* case 2.2.2: csubst0_fst *)
       XReplaceIn H0 i0 i; DropGenBase; NewInduction k; XEAuto.
 (* case 2.2.3: csubst0_both *)
       XReplaceIn H0 i0 i; XReplaceIn H2 i0 i.
@@ -124,9 +123,9 @@ Require Export drop_defs.
 (* case 2.2: n > 0 *)
       Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Clear c1 c2 v y;
       Intros; DropGenBase.
-(* case 2.2.1: csubst0_fst *)
+(* case 2.2.1: csubst0_snd *)
       XEAuto.
-(* case 2.2.2: csubst0_snd *)
+(* case 2.2.2: csubst0_fst *)
       Replace i0 with i; XAuto; XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; Clear H3 i0.
       Apply (r_dis k); Intros; Rewrite (H3 i) in H0; Rewrite (H3 n) in H4.
 (* case 2.2.2.1: bind *)
@@ -158,9 +157,9 @@ Require Export drop_defs.
 (* case 2.2 : n > 0 *)
       Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros;
       DropGenBase.
-(* case 2.2.1 : csubst0_fst *)
+(* case 2.2.1 : csubst0_snd *)
       XAuto.
-(* case 2.2.2 : csubst0_snd *)
+(* case 2.2.2 : csubst0_fst *)
       XReplaceIn H0 i0 i; NewInduction k; XEAuto.
 (* case 2.2.3 : csubst0_both *)
       XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; NewInduction k; XEAuto.