λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / drops_cext2.ma

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 c55f9332fcd09107c6db5e6ae35441610697a238..082cbc824823c868f87119fb7e3ffc1dbb53f3ee 100644 (file)
--- 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-.