λδ-2B is released

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
index 7abac34cd89a9d55f6d60820b4b953878024f853..5a4dd983ca7ffae3d6fcb26b5393b3403b12c82e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
@@ -26,7 +26,7 @@ include "basic_2/rt_computation/rsx_fqup.ma".
 lemma rsx_lifts (h) (G): d_liftable1_isuni … (λL,T. G ⊢ ⬈*[h,T] 𝐒⦃L⦄).
 #h #G #K #T #H @(rsx_ind … H) -K
 #K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @rsx_intro
-#L2 #HL12 #HnL12 elim (lpx_drops_conf … HLK1 … HL12) 
+#L2 #HL12 #HnL12 elim (lpx_drops_conf … HLK1 … HL12)
 /5 width=9 by reqx_lifts_bi, lpx_fwd_length/
 qed-.