(* Basic_1: was just: sn3_abbr *)
(* Basic_2A1: was: csx_lref_bind *)
lemma csx_lref_pair_drops (h) (G):
- â\88\80I,L,K,V,i. â¬\87*[i] L ≘ K.ⓑ{I}V →
+ â\88\80I,L,K,V,i. â\87©*[i] L ≘ K.ⓑ{I}V →
⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄.
#h #G #I #L #K #V #i #HLK #HV
@csx_intro #X #H #Hi elim (cpx_inv_lref1_drops … H) -H
(* Basic_1: was: sn3_gen_def *)
(* Basic_2A1: was: csx_inv_lref_bind *)
lemma csx_inv_lref_pair_drops (h) (G):
- â\88\80I,L,K,V,i. â¬\87*[i] L ≘ K.ⓑ{I}V →
+ â\88\80I,L,K,V,i. â\87©*[i] L ≘ K.ⓑ{I}V →
⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
#h #G #I #L #K #V #i #HLK #Hi
elim (lifts_total V (𝐔❴↑i❵))
lemma csx_inv_lref_drops (h) (G):
∀L,i. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ →
- â\88¨â\88¨ â¬\87*[Ⓕ,𝐔❴i❵] L ≘ ⋆
- | â\88\83â\88\83I,K. â¬\87*[i] L ≘ K.ⓤ{I}
- | â\88\83â\88\83I,K,V. â¬\87*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
+ â\88¨â\88¨ â\87©*[Ⓕ,𝐔❴i❵] L ≘ ⋆
+ | â\88\83â\88\83I,K. â\87©*[i] L ≘ K.ⓤ{I}
+ | â\88\83â\88\83I,K,V. â\87©*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
#h #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/
* * /4 width=9 by csx_inv_lref_pair_drops, ex2_3_intro, ex1_2_intro, or3_intro2, or3_intro1/
qed-.