X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Flib%2Flambda%2Fsubst.ma;fp=matita%2Fmatita%2Flib%2Flambda%2Fsubst.ma;h=4f61ef5282fdcf6da367948d7c264526e7ebf87f;hb=713b0e788ea62b1d130501dbb0441910d2a73492;hp=4258f6a7c5575e5ae6a2ac9dbdc6560d7386b264;hpb=1319bb002c3092e803477f6f7f6f0fa73c2fd6fb;p=helm.git

diff --git a/matita/matita/lib/lambda/subst.ma b/matita/matita/lib/lambda/subst.ma
index 4258f6a7c..4f61ef528 100644
--- a/matita/matita/lib/lambda/subst.ma
+++ b/matita/matita/lib/lambda/subst.ma
@@ -142,6 +142,9 @@ lemma lift_subst_up: ∀M,N,n,i,j.
   ]
 qed.
 
+lemma lift_subst_up_O: ∀v,t,k,p. (lift t (k+1) p)[O≝lift v k p] = lift t[O≝v] k p.
+// qed.
+
 theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → 
   (lift B i (S k)) [j ≝ A] = lift B i k.
 #A #B (elim B) normalize /2/
@@ -202,3 +205,8 @@ lemma subst_lemma: ∀A,B,C.∀k,i.
     ]
   ] 
 qed.
+
+lemma subst_lemma_comm: ∀A,B,C.∀k,i.
+  (A [i ≝ B]) [i+k ≝ C] = (A [i+k+1 := C]) [i ≝ B [k ≝ C]].
+#A #B #C #k #i >commutative_plus >subst_lemma //
+qed.