X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Flifts.ma;h=40158acbe45749e94d83aa002831ccffa248acc4;hb=eae50cc815292d335df1c488a00b39ef98fa5870;hp=f447d729aa027f733bb659aad8779e4c17fcc584;hpb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma
index f447d729a..40158acbe 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma
@@ -61,7 +61,7 @@ qed-.
 
 (* Basic_1: was: lift1_lref *)
 lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 →
-                       ∃∃i2. @[i1] des ≡ i2 & T2 = #i2.
+                       ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
 #T2 #des elim des -des
 [ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/
 | #d #e #des #IH #i1 #H