matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc

   1 (* Advanced inversion lemmas ************************************************)
   2
   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-.
   6
   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-.
  10
  11 (* Advanced eliminators *****************************************************)
  12
  13 lemma lpxs_ind_alt: ∀h,o,G. ∀R:relation lenv.
  14                     R (⋆) (⋆) → (
  15                        ∀I,K1,K2,V1,V2.
  16                        ⦃G, K1⦄ ⊢ ➡*[h, o] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 →
  17                        R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
  18                     ) →
  19                     ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L1 L2.
  20 /3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-.
  21
  22
  23 (* More advanced properties *************************************************)
  24
  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.