update in ground_2, static_2, basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_preserve_sub.ma

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 f86bc1b59cff066761a71a4a30291782cb8d8818..c99d6a5c08a7387f6416eee775775f3b520f73fd 100644 (file)
--- 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):