- advances towards strong normalization

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / lfpx_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma
index 086e71e87bd791fd522681adf3feb065a4419220..d49e4e01d71167d430e4942ea6b0050a2d2a823b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma
@@ -21,7 +21,7 @@ include "basic_2/rt_transition/lfpx.ma".
 (* Properties with generic slicing for local environments *******************)
 
 lemma drops_lfpx_trans: ∀h,G. dedropable_sn (cpx h G).
-/3 width=6 by lfxs_liftable_dedropable, cpx_lifts/ qed-.
+/3 width=6 by lfxs_liftable_dedropable_sn, cpx_lifts_sn/ qed-.
 
 (* Inversion lemmas with generic slicing for local environments *************)