X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_lift.ma;h=e40d8a2824e4e3ee92fa6d764a3dadf8da4b1a1d;hb=6d3e67a714d59ff5d0da7aff72323a6d2ac07db4;hp=854fff7f3448b57640bd4ed09cb613c94afa444e;hpb=28b55bc982671bad6514751c3a368b6cc6cbeec7;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 854fff7f3..e40d8a282 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -77,3 +77,20 @@ lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊢ U ¡[g] → ∀K,d,e. ⇩[d, e] L
   lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/
 ]
 qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma snv_fsup_conf: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+                     ⦃h, L1⦄ ⊢ T1 ¡[g] → ⦃h, L2⦄ ⊢ T2 ¡[g].
+#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 //
+|2,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
+|4,5: * #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-.