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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v
index 5c9c2e5c8..d99a405db 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v
@@ -1,16 +1,24 @@
-(*#* #stop file *)
-
 Require Export lift_defs.
 
+(*#* #caption "axioms for strict substitution in terms",
+   "substituted local reference",
+   "substituted tail item: first operand", 
+   "substituted tail item: second operand", 
+   "substituted tail item: both operands"
+*)
+(*#* #cap #cap t, t1, t2 #alpha v in W, u in V, u1 in V1, u2 in V2, k in z, s in p *)
+
       Inductive subst0 : nat -> T -> T -> T -> Prop :=
-         | subst0_bref : (v:?; i:?) (subst0 i v (TBRef i) (lift (S i) (0) v))
-         | subst0_fst  : (v,w,u:?; i:?) (subst0 i v u w) ->
-                         (t:?; k:?) (subst0 i v (TTail k u t) (TTail k w t))
-         | subst0_snd  : (k:?; v,w,t:?; i:?) (subst0 (s k i) v t w) -> (u:?)
-                         (subst0 i v (TTail k u t) (TTail k u w))
-         | subst0_both : (v,u1,u2:?; i:?) (subst0 i v u1 u2) ->
-                         (k:?; t1,t2:?) (subst0 (s k i) v t1 t2) ->
-                         (subst0 i v (TTail k u1 t1) (TTail k u2 t2)).
+         | subst0_lref: (v:?; i:?) (subst0 i v (TLRef i) (lift (S i) (0) v))
+         | subst0_fst : (v,u2,u1:?; i:?) (subst0 i v u1 u2) ->
+                        (t:?; k:?) (subst0 i v (TTail k u1 t) (TTail k u2 t))
+         | subst0_snd : (k:?; v,t2,t1:?; i:?) (subst0 (s k i) v t1 t2) -> (u:?)
+                        (subst0 i v (TTail k u t1) (TTail k u t2))
+         | subst0_both: (v,u1,u2:?; i:?) (subst0 i v u1 u2) ->
+                        (k:?; t1,t2:?) (subst0 (s k i) v t1 t2) ->
+                        (subst0 i v (TTail k u1 t1) (TTail k u2 t2)).
+
+(*#* #stop file *)
 
       Hint subst0 : ltlc := Constructors subst0.
 
@@ -21,7 +29,7 @@ Require Export lift_defs.
       Intros; Inversion H.
       Qed.
 
-      Theorem subst0_gen_bref : (v,x:?; i,n:?) (subst0 i v (TBRef n) x) ->
+      Theorem subst0_gen_lref : (v,x:?; i,n:?) (subst0 i v (TLRef n) x) ->
                                 n = i /\ x = (lift (S n) (0) v).
       Intros; Inversion H; XAuto.
       Qed.
@@ -46,10 +54,9 @@ Require Export lift_defs.
          Match Context With
             | [ H: (subst0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
                Apply (subst0_gen_sort ?2 ?4 ?1 ?3); Apply H
-            | [ H: (subst0 ?1 ?2 (TBRef ?3) ?4) |- ? ] ->
-               LApply (subst0_gen_bref ?2 ?4 ?1 ?3); [ Clear H; Intros H | XAuto ];
+            | [ H: (subst0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
+               LApply (subst0_gen_lref ?2 ?4 ?1 ?3); [ Clear H; Intros H | XAuto ];
                XElim H; Intros
             | [ H: (subst0 ?1 ?2 (TTail ?3 ?4 ?5) ?6) |- ? ] ->
                LApply (subst0_gen_tail ?3 ?2 ?4 ?5 ?6 ?1); [ Clear H; Intros H | XAuto ];
                XElim H; Intros H; XElim H; Intros.
-