]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma
partial update update in basic_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / lfsx_csx.ma
index 5310d8ab791aac77a0b133907090ed8a605fee55..bdaca97bc7657d4cfb25f0558f7b2c8e46fdbb21 100644 (file)
@@ -19,7 +19,7 @@ include "basic_2/rt_computation/csx_lsubr.ma".
 include "basic_2/rt_computation/lfsx_lpx.ma".
 include "basic_2/rt_computation/lsubsx_lfsx.ma".
 
-(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
 
 (* Advanced properties ******************************************************)
 
@@ -44,7 +44,7 @@ qed.
 
 (* Basic_2A1: uses: lsx_lref_be *)
 lemma lfsx_lref_pair_drops: ∀h,o,G,K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ →
-                            â\88\80I,i,L. â¬\87*[i] L â\89¡ K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
+                            â\88\80I,i,L. â¬\87*[i] L â\89\98 K.ⓑ{I}V → G ⊢ ⬈*[h, o, #i] 𝐒⦃L⦄.
 #h #o #G #K #V #HV #HK #I #i elim i -i
 [ #L #H >(drops_fwd_isid … H) -H /2 width=3 by lfsx_pair_lpxs/
 | #i #IH #L #H