1 (* Advanced inversion lemmas ************************************************)
3 lemma lpxs_inv_pair1: ∀h,o,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2 →
4 ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L2 = K2.ⓑ{I}V2.
5 /3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-.
7 lemma lpxs_inv_pair2: ∀h,o,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, o] K2.ⓑ{I}V2 →
8 ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L1 = K1.ⓑ{I}V1.
9 /3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-.
11 (* Advanced eliminators *****************************************************)
13 lemma lpxs_ind_alt: ∀h,o,G. ∀R:relation lenv.
16 ⦃G, K1⦄ ⊢ ➡*[h, o] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 →
17 R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
19 ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L1 L2.
20 /3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-.
23 (* More advanced properties *************************************************)
25 lemma lpxs_pair2: ∀h,o,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 →
26 ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, o] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V2.
27 /3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.