- degree assignment, static type assignment, iterated static type

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / csn_lpx.ma

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 c4e156e9bf9c12dc398247586418f117209fe733..0fbc4c66f10ebfb5c5a046aa4bc9a33ef720a893 100644 (file)
--- 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/
 ]