(* Properties on relocation *************************************************)
-lemma crx_lift: â\88\80h,g,G,K,T. â¦\83G, Kâ¦\84 â\8a¢ â\9e¡[h, g] ð\9d\90\91â¦\83Tâ¦\84 â\86\92 â\88\80L,s,d,e. â\87©[s, d, e] L ≡ K →
- â\88\80U. â\87§[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄.
+lemma crx_lift: â\88\80h,g,G,K,T. â¦\83G, Kâ¦\84 â\8a¢ â\9e¡[h, g] ð\9d\90\91â¦\83Tâ¦\84 â\86\92 â\88\80L,s,d,e. â¬\87[s, d, e] L ≡ K →
+ â\88\80U. â¬\86[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄.
#h #g #G #K #T #H elim H -K -T
[ #K #k #l #Hkl #L #s #d #e #_ #X #H
>(lift_inv_sort1 … H) -X /2 width=2 by crx_sort/
]
qed.
-lemma crx_inv_lift: â\88\80h,g,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â\9e¡[h, g] ð\9d\90\91â¦\83Uâ¦\84 â\86\92 â\88\80K,s,d,e. â\87©[s, d, e] L ≡ K →
- â\88\80T. â\87§[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
+lemma crx_inv_lift: â\88\80h,g,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â\9e¡[h, g] ð\9d\90\91â¦\83Uâ¦\84 â\86\92 â\88\80K,s,d,e. â¬\87[s, d, e] L ≡ K →
+ â\88\80T. â¬\86[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
#h #g #G #L #U #H elim H -L -U
[ #L #k #l #Hkl #K #s #d #e #_ #X #H
>(lift_inv_sort2 … H) -X /2 width=2 by crx_sort/