X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Flifts_lift_vector.ma;h=7d14197474b0acad3e0aa9042cfcfc24e674f0fa;hb=8ff4315142253a1a0478b67c07dddf70c36f50cd;hp=bbd3b1d8ba1261ca6589cd29f94fecde6880f264;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift_vector.ma
index bbd3b1d8b..7d1419747 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lifts_lift_vector.ma
@@ -23,7 +23,7 @@ include "basic_2/unfold/lifts_vector.ma".
 (* Basic_1: was: lifts1_xhg (right to left) *)
 lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts →
                              ∀T2s:list term. ⇧[0, 1] Ts ≡ T2s →
-                             ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[des + 1] T0s ≡ T2s. 
+                             ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[des + 1] T0s ≡ T2s.
 #T1s #Ts #des #H elim H -T1s -Ts
 [ #T1s #H
   >(liftv_inv_nil1 … H) -T1s /2 width=3/