(* 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 //
]
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 (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/
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-.