X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpr_drops.ma;h=c7c28703669fb4fde68ed1cc7cdde314bcef77ab;hb=09b4420070d6a71990e16211e499b51dbb0742cb;hp=48d281e4f27144c0a292c36af19b191ecbfa3570;hpb=bba53a83579540bc3925d47d679e2aad22e85755;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma
index 48d281e4f..c7c287036 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma
@@ -27,7 +27,7 @@ lemma cpr_inv_atom1_drops: ∀h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[h] T2 →
 [ /2 width=1 by or_introl/
 | #s #_ #_ #H destruct
 | /3 width=8 by ex4_4_intro, or_intror/
-| #m #K #V1 #V2 #i #_ #_ #_ #_ #H destruct
+| #k #K #V1 #V2 #i #_ #_ #_ #_ #H destruct
 ]
 qed-.
 
@@ -40,6 +40,6 @@ lemma cpr_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h] T2 →
 #h #G #L #T2 #i #H elim (cpm_inv_lref1_drops … H) -H *
 [ /2 width=1 by or_introl/
 | /3 width=6 by ex3_3_intro, or_intror/
-| #m #K #V1 #V2 #_ #_ #_ #H destruct
+| #k #K #V1 #V2 #_ #_ #_ #H destruct
 ]
 qed-.