X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpxs_theq.ma;h=ae05d817e9fb5a37390a43425391f3558554cf43;hb=730642efca3fb00ca4f8268bd97b0778cff14514;hp=8a52882a2b5ef4ca58dedb110a99088cdbfe294f;hpb=6555775aa5268dec0d9ae4579412b659cacdc964;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma
index 8a52882a2..ae05d817e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma
@@ -15,9 +15,9 @@
 include "basic_2/syntax/theq_tdeq.ma".
 include "basic_2/rt_computation/cpxs_lsubr.ma".
 include "basic_2/rt_computation/cpxs_cnx.ma".
-include "basic_2/rt_computation/lfpxs_cpxs.ma".
+include "basic_2/rt_computation/lpxs_cpxs.ma".
 
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
 
 (* Forward lemmas with head equivalence for terms ***************************)
 
@@ -32,8 +32,8 @@ qed-.
 
 (* Note: probably this is an inversion lemma *)
 (* Basic_2A1: was: cpxs_fwd_delta *)
-lemma cpxs_fwd_delta_drops: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 →
-                            ∀V2. ⬆*[⫯i] V1 ≡ V2 →
+lemma cpxs_fwd_delta_drops: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
+                            ∀V2. ⬆*[↑i] V1 ≘ V2 →
                             ∀U. ⦃G, L⦄ ⊢ #i ⬈*[h] U →
                             #i ⩳[h, o] U ∨ ⦃G, L⦄ ⊢ V2 ⬈*[h] U.
 #h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H
@@ -58,7 +58,7 @@ lemma cpxs_fwd_beta: ∀h,o,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h]
 qed-.
 
 lemma cpxs_fwd_theta: ∀h,o,p,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] U →
-                      ∀V2. ⬆*[1] V1 ≡ V2 → ⓐV1.ⓓ{p}V.T ⩳[h, o] U ∨
+                      ∀V2. ⬆*[1] V1 ≘ V2 → ⓐV1.ⓓ{p}V.T ⩳[h, o] U ∨
                       ⦃G, L⦄ ⊢ ⓓ{p}V.ⓐV2.T ⬈*[h] U.
 #h #o #p #G #L #V1 #V #T #U #H #V2 #HV12
 elim (cpxs_inv_appl1 … H) -H *