X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Faaa_aaa.ma;h=66d0f47d9f3d7de450db97fae52d24867a80102d;hb=93bba1c94779e83184d111cd077d4167e42a74aa;hp=76bf7e529eb04fdaebadcf601b98addc9c729b0f;hpb=9a023f554e56d6edbbb2eeaf17ce61e31857ef4a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
index 76bf7e529..66d0f47d9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
@@ -21,7 +21,7 @@ include "basic_2/static/aaa.ma".
 
 theorem aaa_mono: ∀G,L,T,A1. ⦃G, L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T ⁝ A2 → A1 = A2.
 #G #L #T #A1 #H elim H -G -L -T -A1
-[ #G #L #k #A2 #H
+[ #G #L #s #A2 #H
   >(aaa_inv_sort … H) -H //
 | #I1 #G #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H
   elim (aaa_inv_lref … H) -H #I2 #K2 #V2 #HLK2 #HA2