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=6d79ef571086474dc30eb177f1c0bb8684d5653a;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;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 6d79ef571..0a1feae91 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/xprs_lift.ma".
+include "basic_2/computation/dxprs_lift.ma".
 include "basic_2/equivalence/cpcs_cpcs.ma".
 include "basic_2/dynamic/snv.ma".
 
@@ -20,8 +20,8 @@ include "basic_2/dynamic/snv.ma".
 
 (* Relocation properties ****************************************************)
 
-lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡ K →
-                ∀U. ⇧[d, e] T ≡ U → ⦃h, L⦄ ⊩ U :[g].
+lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊢ T ¡[g] → ∀L,d,e. ⇩[d, e] L ≡ K →
+                ∀U. ⇧[d, e] T ≡ U → ⦃h, L⦄ ⊢ U ¡[g].
 #h #g #K #T #H elim H -K -T
 [ #K #k #L #d #e #_ #X #H
   >(lift_inv_sort1 … H) -X -K -d -e //
@@ -42,7 +42,7 @@ lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡
   elim (lift_total T1 (d+1) e) #U1 #HTU1
   @(snv_appl … a … W0 … W1 … U1 l)
   [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ]
-  @(xprs_lift … HLK … HTU … HT1) /2 width=1/
+  @(dxprs_lift … HLK … HTU … HT1) /2 width=1/
 | #K #V0 #T #V #l #_ #_ #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H
   elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct
   elim (lift_total V d e) #W #HVW
@@ -50,8 +50,8 @@ lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡
 ]
 qed.
 
-lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L ≡ K →
-                    ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊩ T :[g].
+lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊢ U ¡[g] → ∀K,d,e. ⇩[d, e] L ≡ K →
+                    ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊢ T ¡[g].
 #h #g #L #U #H elim H -L -U
 [ #L #k #K #d #e #_ #X #H
   >(lift_inv_sort2 … H) -X -L -d -e //
@@ -67,8 +67,8 @@ lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L
 | #a #L #W #W0 #W1 #U #U1 #l #_ #_ #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
   elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HV0 #HVW0
-  elim (cprs_inv_lift1 … HLK … HVW0 … HW01) -W0 #V1 #HVW1 #HV01
-  elim (xprs_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU
+  elim (cprs_inv_lift1 … HW01 … HLK … HVW0) -W0 #V1 #HVW1 #HV01
+  elim (dxprs_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU
   elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct
   lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=8/
 | #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H
@@ -77,3 +77,22 @@ 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: *
+|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 //
+  ]
+]
+qed-.