X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_preserve.ma;h=ebc6fd96db1b50b6f73aba63dcd70f8da0c7f37d;hp=0d058a6733b3540efad5626fd07903b90a60e87c;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
index 0d058a673..ebc6fd96d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
@@ -125,7 +125,7 @@ elim (cpms_inv_lref_sn … H2) -H2 *
 qed-.
 
 lemma nta_inv_lref_sn_drops_cnv (a) (h) (G) (L): 
-      ∀X2, i. ⦃G,L⦄ ⊢ #i :[a,h] X2 →
+      ∀X2,i. ⦃G,L⦄ ⊢ #i :[a,h] X2 →
       ∨∨ ∃∃K,V,W,U. ⬇*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V :[a,h] W & ⬆*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h]
        | ∃∃K,W,U. ⬇*[i] L ≘ K. ⓛW & ⦃G,K⦄ ⊢ W ![a,h] & ⬆*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h].
 #a #h #G #L #X2 #i #H
@@ -241,7 +241,7 @@ elim (cpms_inv_cast1 … H2) -H2 [ * || * ]
 qed-.
 
 (* Basic_1: uses: ty3_gen_lift *)
-(* Note: "⦃G,L⦄ ⊢ U2 ⬌*[h] X2" can be "⦃G,L⦄ ⊢ X2 ➡*[h] U2" *)
+(* Note: "⦃G, L⦄ ⊢ U2 ⬌*[h] X2" can be "⦃G, L⦄ ⊢ X2 ➡*[h] U2" *)
 lemma nta_inv_lifts_sn (a) (h) (G):
       ∀L,T2,X2. ⦃G,L⦄ ⊢ T2 :[a,h] X2 →
       ∀b,f,K. ⬇*[b,f] L ≘ K → ∀T1. ⬆*[f] T1 ≘ T2 →