X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fdrops_cext2.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Fdrops_cext2.ma;h=082cbc824823c868f87119fb7e3ffc1dbb53f3ee;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=c55f9332fcd09107c6db5e6ae35441610697a238;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_cext2.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_cext2.ma
index c55f9332f..082cbc824 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_cext2.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_cext2.ma
@@ -26,4 +26,4 @@ lemma cext2_d_liftable2_sn: ∀R. d_liftable2_sn … lifts R →
 | lapply (liftsb_inv_pair_sn … H) * #U1 #HTU1
 ] -H #H destruct /3 width=3 by ext2_unit, ex2_intro/
 elim (HR … HT12 … HLK … HTU1) -HR -b -K -T1 /3 width=3 by ext2_pair, ex2_intro/
-qed-. 
+qed-.