qed.
lemma cpx_lref: ∀h,I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T →
- â¬\86*[1] T â\89\98 U â\86\92 â¦\83G, K.â\93\98{I}â¦\84 â\8a¢ #⫯i ⬈[h] U.
+ â¬\86*[1] T â\89\98 U â\86\92 â¦\83G, K.â\93\98{I}â¦\84 â\8a¢ #â\86\91i ⬈[h] U.
#h #I #G #K #T #U #i *
/3 width=4 by cpg_lref, ex_intro/
qed.
| ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≘ T2 &
L = K.ⓑ{I}V1 & J = LRef 0
| ∃∃I,K,T,i. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≘ T2 &
- L = K.â\93\98{I} & J = LRef (⫯i).
+ L = K.â\93\98{I} & J = LRef (â\86\91i).
#h #J #G #L #T2 * #c #H elim (cpg_inv_atom1 … H) -H *
/4 width=8 by or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex4_4_intro, ex2_intro, ex_intro/
qed-.
/4 width=7 by ex3_4_intro, ex_intro, or_introl, or_intror/
qed-.
-lemma cpx_inv_lref1: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i ⬈[h] T2 →
- â\88¨â\88¨ T2 = #(⫯i)
+lemma cpx_inv_lref1: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #â\86\91i ⬈[h] T2 →
+ â\88¨â\88¨ T2 = #(â\86\91i)
| ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≘ T2 & L = K.ⓘ{I}.
#h #G #L #T2 #i * #c #H elim (cpg_inv_lref1 … H) -H *
/4 width=6 by ex3_3_intro, ex_intro, or_introl, or_intror/
/4 width=3 by ex2_intro, ex_intro, or_intror, or_introl/
qed-.
-lemma cpx_inv_lref1_bind: â\88\80h,I,G,K,T2,i. â¦\83G, K.â\93\98{I}â¦\84 â\8a¢ #⫯i ⬈[h] T2 →
- â\88¨â\88¨ T2 = #(⫯i)
+lemma cpx_inv_lref1_bind: â\88\80h,I,G,K,T2,i. â¦\83G, K.â\93\98{I}â¦\84 â\8a¢ #â\86\91i ⬈[h] T2 →
+ â\88¨â\88¨ T2 = #(â\86\91i)
| ∃∃T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≘ T2.
#h #I #G #L #T2 #i * #c #H elim (cpg_inv_lref1_bind … H) -H *
/4 width=3 by ex2_intro, ex_intro, or_introl, or_intror/
(∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → R G K V1 V2 →
⬆*[1] V2 ≘ W2 → R G (K.ⓑ{I}V1) (#0) W2
) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → R G K (#i) T →
- â¬\86*[1] T â\89\98 U â\86\92 R G (K.â\93\98{I}) (#⫯i) (U)
+ â¬\86*[1] T â\89\98 U â\86\92 R G (K.â\93\98{I}) (#â\86\91i) (U)
) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →
R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →