- degree-based equivalene for terms

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpr_drops.ma

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 48d281e4f27144c0a292c36af19b191ecbfa3570..c7c28703669fb4fde68ed1cc7cdde314bcef77ab 100644 (file)
--- 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-.