- the shift function is now defined and cpr_shift_fwd is proved

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / reduction / tpr_lift.ma

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 f3afe6f214a252de15ed6be1eecc951c4a6cdb1c..a748416f00e9369576347893e1765bac4ff801a8 100644 (file)
--- 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