-lemma cpxs_inv_lref1: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i ⬈*[h] T2 →
- T2 = #(⫯i) ∨
- â\88\83â\88\83I,K,T. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88*[h] T & â¬\86*[1] T â\89¡ T2 & L = K.ⓘ{I}.
+lemma cpxs_inv_lref1: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #â\86\91i ⬈*[h] T2 →
+ T2 = #(â\86\91i) ∨
+ â\88\83â\88\83I,K,T. â¦\83G, Kâ¦\84 â\8a¢ #i â¬\88*[h] T & â¬\86*[1] T â\89\98 T2 & L = K.ⓘ{I}.