substitution lemma for stratified native validity!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reducibility / cfpr_ltpss.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma
index 424911376fa48480f7edea29c65e4222d8c590a6..785aefd5178dadb64d0ea1f9bfe8075c5952b4bf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/reducibility/cpr_lift.ma".
-include "basic_2/reducibility/cpr_ltpss.ma".
+include "basic_2/reducibility/cpr_ltpss_sn.ma".
 include "basic_2/reducibility/cfpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************)