- the shift function is now defined and cpr_shift_fwd is proved

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / substitution / tps_lift.ma

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 24571a88f48a1b3fe45b08c0ad249e68222e4df9..1fc78227d0d0b3bba622a0c342aca2e0c92f0450 100644 (file)
--- 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
 [ //
 | //