| ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 & ⬆*[1] V2 ≘ T2 &
L = K.ⓓ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 #H elim (cpm_inv_atom1 … H) -H *
/3 width=8 by tri_lt, or3_intro0, or3_intro1, or3_intro2, ex4_4_intro, ex4_3_intro/
#n #_ #_ #H destruct
#n #K #V1 #V2 #_ #_ #_ #H destruct
qed-.
-lemma cpr_inv_lref1: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i ➡[h] T2 →
- â\88¨â\88¨ T2 = #(⫯i)
+lemma cpr_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 #H elim (cpm_inv_lref1 … H) -H *
/3 width=6 by ex3_3_intro, or_introl, or_intror/