(* Relocation properties ****************************************************)
-lemma snv_lift: â\88\80h,g,G,K,T. â¦\83G, Kâ¦\84 â\8a¢ T ¡[h, g] â\86\92 â\88\80L,s,d,e. â\87©[s, d, e] L ≡ K →
- â\88\80U. â\87§[d, e] T ≡ U → ⦃G, L⦄ ⊢ U ¡[h, g].
+lemma snv_lift: â\88\80h,g,G,K,T. â¦\83G, Kâ¦\84 â\8a¢ T ¡[h, g] â\86\92 â\88\80L,s,d,e. â¬\87[s, d, e] L ≡ K →
+ â\88\80U. â¬\86[d, e] T ≡ U → ⦃G, L⦄ ⊢ U ¡[h, g].
#h #g #G #K #T #H elim H -G -K -T
[ #G #K #k #L #s #d #e #_ #X #H
>(lift_inv_sort1 … H) -X -K -d -e //
| #G #K #V #T #U0 #_ #_ #HVU0 #HTU0 #IHV #IHT #L #s #d #e #HLK #X #H
elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
elim (lift_total U0 d e)
- /3 width=12 by snv_cast, cprs_lift, scpds_lift/
+ /3 width=12 by snv_cast, scpds_lift/
]
qed.
-lemma snv_inv_lift: â\88\80h,g,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ U ¡[h, g] â\86\92 â\88\80K,s,d,e. â\87©[s, d, e] L ≡ K →
- â\88\80T. â\87§[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g].
+lemma snv_inv_lift: â\88\80h,g,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ U ¡[h, g] â\86\92 â\88\80K,s,d,e. â¬\87[s, d, e] L ≡ K →
+ â\88\80T. â¬\86[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g].
#h #g #G #L #U #H elim H -G -L -U
[ #G #L #k #K #s #d #e #_ #X #H
>(lift_inv_sort2 … H) -X -L -d -e //
/3 width=6 by snv_appl/
| #G #L #W #U #U1 #_ #_ #HWU1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
- elim (cprs_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0
+ elim (scpds_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0
elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #HX #HTU0
lapply (lift_inj … HX … HU01) -HX #H destruct
/3 width=5 by snv_cast/