X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_lift.ma;h=0a1feae918756b4cb9fbddfa298f9090cc838af8;hb=90ee1e85245752414b93826aabe388409571187a;hp=966760b80ea4e616c296806c8e3d26fe08838d29;hpb=874cacec64d0aab52ab1a21aad23208f52f50caf;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
index 966760b80..0a1feae91 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -86,11 +86,13 @@ lemma snv_fsup_conf: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
 [ #I1 #L1 #V1 #H
   elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2
   lapply (ldrop_inv_refl … H) -H #H destruct //
-|2,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
-|4,5: * #L1 #V1 #T1 #H
+|2: *
+|5: /3 width=7 by snv_inv_lift/
+]
+[1,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
+|2,4: * #L1 #V1 #T1 #H
   [1,3: elim (snv_inv_appl … H) -H //
   |2,4: elim (snv_inv_cast … H) -H //
   ]
-| /3 width=7 by snv_inv_lift/
 ]
 qed-.