X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcsn_lpx.ma;h=0fbc4c66f10ebfb5c5a046aa4bc9a33ef720a893;hb=fdb2c62b58006b82c015ba70b494d50c7860e28f;hp=c4e156e9bf9c12dc398247586418f117209fe733;hpb=4aa431513ffa0ce0accf81e6e9ea4b9314d468e3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma
index c4e156e9b..0fbc4c66f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma
@@ -35,7 +35,7 @@ lemma csn_abst: ∀h,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
 elim (cpx_inv_abst1 … H1) -H1
 #W0 #T0 #HLW0 #HLT0 #H destruct
 elim (eq_false_inv_tpair_sn … H2) -H2
-[ -IHT #H lapply (csn_cpx_trans … HLT0) // -HT 
+[ -IHT #H lapply (csn_cpx_trans … HLT0) // -HT
   #HT0 lapply (csn_lpx_conf … (L.ⓛW0) … HT0) -HT0 /2 width=1/ /3 width=1/
 | -IHW -HLW0 -HT * #H destruct /3 width=1/
 ]