X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Fsubstitution%2Ftps_lift.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Fsubstitution%2Ftps_lift.ma;h=1fc78227d0d0b3bba622a0c342aca2e0c92f0450;hb=b264ad188cb0023a16dae105b037357fa75c5c1a;hp=24571a88f48a1b3fe45b08c0ad249e68222e4df9;hpb=ffe34220d80cba65eccf2396fba7f692cc6448c8;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
index 24571a88f..1fc78227d 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
@@ -184,8 +184,8 @@ qed.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma tps_inv_refl1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
-                         ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+fact tps_inv_refl1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
+                        ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
 #L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
 [ //
 | //