update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / snv_lift.ma

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 0a1feae918756b4cb9fbddfa298f9090cc838af8..8b68e242cf64b043f32620ff3ee445a12312b5a9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -85,9 +85,9 @@ lemma snv_fsup_conf: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
 #h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
 [ #I1 #L1 #V1 #H
   elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2
-  lapply (ldrop_inv_refl … H) -H #H destruct //
+  lapply (ldrop_inv_O2 … H) -H #H destruct //
 |2: *
-|5: /3 width=7 by snv_inv_lift/
+|5,6: /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