X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpts_drops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpts_drops.ma;h=cebbb8ed0b11ea65df0287f581ab502a353d7188;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=66045be0e99912b9df193d2241f3274def2acdf6;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma
index 66045be0e..cebbb8ed0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma
@@ -24,7 +24,7 @@ lemma cpts_lifts_sn (h) (n) (G):
       d_liftable2_sn … lifts (λL. cpts h G L n).
 /3 width=6 by d2_liftable_sn_ltc, cpt_lifts_sn/ qed-.
 
-lemma cpts_lifts_bi (h) (n) (G): 
+lemma cpts_lifts_bi (h) (n) (G):
       d_liftable2_bi … lifts (λL. cpts h G L n).
 #h #n #G @d_liftable2_sn_bi
 /2 width=6 by cpts_lifts_sn, lifts_mono/