- predefined_virtuals: an addition

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / static / aaa_lifts.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma
index cc18036725eeffce7b98e9ad43b5a78bee896adf..7514f6dc5f7e7ae084f92882a3a13581c42f728f 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma
@@ -20,7 +20,7 @@ include "basic_2/static/aaa_lift.ma".
 (* Properties concerning generic relocation *********************************)
 
 lemma aaa_lifts: ∀L1,L2,T2,A,des. ⇩*[des] L2 ≡ L1 → ∀T1. ⇧*[des] T1 ≡ T2 →
-                                  L1 ⊢ T1 ÷ A →  L2 ⊢ T2 ÷ A.
+                                  L1 ⊢ T1 ⁝ A →  L2 ⊢ T2 ⁝ A.
 #L1 #L2 #T2 #A #des #H elim H -L1 -L2 -des
 [ #L #T1 #H #HT1
   <(lifts_inv_nil … H) -H //