X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcnr_tdeq.ma;h=80e4d8ff02f0cb5a6ce1ed917bf62d034c8f551f;hp=3efc47bba7ed5ed55556eb33b4525a7a7b883c92;hb=31be09cc0d040577917783e050e1d38c0daa8f01;hpb=bf2b1df641df98a3b614a8c3d53edee8beb0964a

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma
index 3efc47bba..80e4d8ff0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma
@@ -82,7 +82,7 @@ lemma cnr_dec_tdeq (h) (G) (L):
         elim (tdeq_inv_pair … H) -H #H destruct
       | @or_intror @(ex2_intro … (ⓓ{p}ⓝW1.V1.U1)) [ /2 width=1 by cpm_beta/ ] #H
         elim (tdeq_inv_pair … H) -H #H destruct
-      ] 
+      ]
     | #T2 #HT12 #HnT12 #_
       @or_intror @(ex2_intro … (ⓐV1.T2)) [ /2 width=1 by cpm_appl/ ] #H
       elim (tdeq_inv_pair … H) -H /2 width=1 by/