X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Freduction%2Ftpr_lift.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Freduction%2Ftpr_lift.ma;h=a748416f00e9369576347893e1765bac4ff801a8;hb=b264ad188cb0023a16dae105b037357fa75c5c1a;hp=f3afe6f214a252de15ed6be1eecc951c4a6cdb1c;hpb=ffe34220d80cba65eccf2396fba7f692cc6448c8;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
index f3afe6f21..a748416f0 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
@@ -96,8 +96,8 @@ qed.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 →
-                         ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
+fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 →
+                        ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
 #U1 #U2 * -U1 U2
 [ #k #V #T #H destruct
 | #i #V #T #H destruct