X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Fxpr_lift.ma;h=1f2bdb130e81b83776f4ac56e449bce0f651bae6;hb=cc21d0caa6229b7d1a905f9b62de2af4f40cc863;hp=9b1376aaa34e456175bed4f938ab75a2bae734f7;hpb=5ea90cbbb01fe0bf3b77221d9e6c87002982621f;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma
index 9b1376aaa..1f2bdb130 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma
@@ -20,10 +20,10 @@ include "basic_2/reducibility/xpr.ma".
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma xpr_inv_abst1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛV1.T1 ➸[g] U2 →
+lemma xpr_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 ➸[g] U2 →
                      ∃∃V2,T2. L ⊢ V1 ➡ V2 & ⦃h, L. ⓛV1⦄ ⊢ T1 ➸[g] T2 &
-                              U2 = ⓛV2. T2.
-#h #g #L #V1 #T1 #U2 *
+                              U2 = ⓛ{a}V2. T2.
+#h #g #a #L #V1 #T1 #U2 *
 [ #H elim (cpr_inv_abst1 … H Abst V1) /3 width=5/
 | * #l #H elim (ssta_inv_bind1 … H) /3 width=5/
 ]