milestone in basic_2 with additions in static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cnr_tdeq.ma

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 3efc47bba7ed5ed55556eb33b4525a7a7b883c92..80e4d8ff02f0cb5a6ce1ed917bf62d034c8f551f 100644 (file)
--- 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/