substitution lemma for stratified native validity!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cprs_lfpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma
index 1ba4cadd8202a687c7e1968136ce8a013fab3a1f..799ec7bc62fd2e3fa960e10ef7c5c9ee3595acd6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lfpr.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/reducibility/ltpr_tps.ma".
-include "basic_2/reducibility/cpr_ltpss.ma".
+include "basic_2/reducibility/cpr_ltpss_sn.ma".
 include "basic_2/reducibility/lfpr.ma".
 include "basic_2/computation/cprs.ma".