X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_preserve_sub.ma;h=c99d6a5c08a7387f6416eee775775f3b520f73fd;hp=f86bc1b59cff066761a71a4a30291782cb8d8818;hb=b98ec1a1a37602eca524dc5487c357a200bbb5b6;hpb=eeeaecfafd5ddffa54a41356104fbc60369e5d73

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma
index f86bc1b59..c99d6a5c0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma
@@ -12,8 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/rt_computation/fpbg.ma".
-include "basic_2/rt_computation/cpms_fpbs.ma".
+include "basic_2/rt_computation/cpms_fpbg.ma".
 include "basic_2/dynamic/cnv.ma".
 
 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
@@ -56,7 +55,7 @@ fact cnv_cpms_trans_lpr_sub (a) (h) (o):
                             ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
 #a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
 @(cpms_ind_dx … H) -n -T2
-/4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/
+/3 width=7 by fpbg_cpms_trans/
 qed-.
 
 fact cnv_cpm_conf_lpr_sub (a) (h) (o):