X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_preserve.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_preserve.ma;h=20bb43faffc51222977602b3f4b8fe7b89ec24fc;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=44dac970e116e598f4c4c4fe13a309953588ce2f;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;p=helm.git

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 44dac970e..20bb43faf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
@@ -124,7 +124,7 @@ elim (cpms_inv_lref_sn … H2) -H2 *
 ]
 qed-.
 
-lemma nta_inv_lref_sn_drops_cnv (h) (a) (G) (L): 
+lemma nta_inv_lref_sn_drops_cnv (h) (a) (G) (L):
       ∀X2,i. ⦃G,L⦄ ⊢ #i :[h,a] X2 →
       ∨∨ ∃∃K,V,W,U. ⇩*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V :[h,a] W & ⇧*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a]
        | ∃∃K,W,U. ⇩*[i] L ≘ K. ⓛW & ⦃G,K⦄ ⊢ W ![h,a] & ⇧*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h,a].