X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fequivalence%2Fcpcs.ma;h=e8ecc622c339fa50d052936b709803806e9be15f;hb=7ad8c044ab33ea0f2aebb1c40fa20340d7f2f3eb;hp=deb838412475787db957296e500fc9ba864ac64a;hpb=a5b0e6d1efb9b5126cc1d72d954edc9a5e630981;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
index deb838412..e8ecc622c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
@@ -85,7 +85,7 @@ lemma cpcs_cpr_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄
 (* Basic_1: removed theorems 9:
             clear_pc3_trans pc3_ind_left
             pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21
-            pc3_pr2_fsubst0 pc3_pr2_fsubst0_back pc3_fsubst0
+            pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0
             pc3_gen_abst pc3_gen_abst_shift
 *)
 (* Basic_1: removed local theorems 6: