(* *)
(**************************************************************************)
-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".
(* Relocation properties ****************************************************)
-lemma snv_lift: â\88\80h,g,K,T. â¦\83h, Kâ¦\84 â\8a© T :[g] → ∀L,d,e. ⇩[d, e] L ≡ K →
- â\88\80U. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Lâ¦\84 â\8a© U :[g].
+lemma snv_lift: â\88\80h,g,K,T. â¦\83h, Kâ¦\84 â\8a¢ T ¡[g] → ∀L,d,e. ⇩[d, e] L ≡ K →
+ â\88\80U. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Lâ¦\84 â\8a¢ 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 //
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
]
qed.
-lemma snv_inv_lift: â\88\80h,g,L,U. â¦\83h, Lâ¦\84 â\8a© U :[g] → ∀K,d,e. ⇩[d, e] L ≡ K →
- â\88\80T. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Kâ¦\84 â\8a© T :[g].
+lemma snv_inv_lift: â\88\80h,g,L,U. â¦\83h, Lâ¦\84 â\8a¢ U ¡[g] → ∀K,d,e. ⇩[d, e] L ≡ K →
+ â\88\80T. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Kâ¦\84 â\8a¢ 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 //
| #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
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_O2 … H) -H #H destruct //
+|2: *
+|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
+ [1,3: elim (snv_inv_appl … H) -H //
+ |2,4: elim (snv_inv_cast … H) -H //
+ ]
+]
+qed-.