- advances towards strong normalization

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma
index 3156e7252cf303c9721374975a84951a3919e93f..7d23f3b0f8cf5e829d601db46e2c8012da168b1a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma
@@ -21,7 +21,7 @@ include "basic_2/rt_transition/lfpr.ma".
 (* Properties with generic slicing for local environments *******************)
 
 lemma drops_lfpr_trans: ∀h,G. dedropable_sn (cpm 0 h G).
-/3 width=6 by lfxs_liftable_dedropable, cpm_lifts/ qed-.
+/3 width=6 by lfxs_liftable_dedropable_sn, cpm_lifts_sn/ qed-.
 
 (* Inversion lemmas with generic slicing for local environments *************)