λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpts_drops.ma

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 66045be0e99912b9df193d2241f3274def2acdf6..cebbb8ed0b11ea65df0287f581ab502a353d7188 100644 (file)
--- 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/