X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fequivalence%2Fcpcs_cpcs.ma;h=6e098196b466933ca82809fdd44ac5e2d13b556d;hb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;hp=784dfb0298ec484fbb56e49ea2f7b500ae56ed8d;hpb=3a430d712f9d87185e9271b7b0c5188c5f311e4b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
index 784dfb029..6e098196b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
@@ -59,10 +59,10 @@ elim (cprs_inv_abst1 … H2) -H2 #W0 #T0 #_ #_ #H destruct
 qed-.
 
 (* Basic_1: was: pc3_gen_lift *)
-lemma cpcs_inv_lift: ∀G,L,K,c,l,k. ⬇[c, l, k] L ≡ K →
+lemma cpcs_inv_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≡ K →
                      ∀T1,U1. ⬆[l, k] T1 ≡ U1 → ∀T2,U2. ⬆[l, k] T2 ≡ U2 →
                      ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2.
-#G #L #K #c #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
+#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
 elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2
 elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
 elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU
@@ -150,10 +150,10 @@ lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 →
 qed-.
 
 (* Basic_1: was: pc3_lift *)
-lemma cpcs_lift: ∀G,L,K,c,l,k. ⬇[c, l, k] L ≡ K →
+lemma cpcs_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≡ K →
                  ∀T1,U1. ⬆[l, k] T1 ≡ U1 → ∀T2,U2. ⬆[l, k] T2 ≡ U2 →
                  ⦃G, K⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ U1 ⬌* U2.
-#G #L #K #c #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12
+#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12
 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
 elim (lift_total T l k) /3 width=12 by cprs_div, cprs_lift/
 qed.