X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcpr.ma;h=d5374513aa6a6d8aff14b368ba9fe7cd1e9c17a2;hb=93bba1c94779e83184d111cd077d4167e42a74aa;hp=27682aa7432444449da3c22004d2e6bf45a92549;hpb=9a023f554e56d6edbbb2eeaf17ce61e31857ef4a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
index 27682aa74..d5374513a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
@@ -131,8 +131,8 @@ lemma cpr_inv_atom1: ∀I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡ T2 →
 /2 width=3 by cpr_inv_atom1_aux/ qed-.
 
 (* Basic_1: includes: pr0_gen_sort pr2_gen_sort *)
-lemma cpr_inv_sort1: ∀G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ➡ T2 → T2 = ⋆k.
-#G #L #T2 #k #H
+lemma cpr_inv_sort1: ∀G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡ T2 → T2 = ⋆s.
+#G #L #T2 #s #H
 elim (cpr_inv_atom1 … H) -H //
 * #K #V #V2 #i #_ #_ #_ #H destruct
 qed-.