- bug fix in notation precedences

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / lifts.ma

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 f447d729aa027f733bb659aad8779e4c17fcc584..40158acbe45749e94d83aa002831ccffa248acc4 100644 (file)
--- 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