-lemma lfpxs_lfdneq_inv_step_sn: â\88\80h,o,G,L1,L2,T. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L2 â\86\92 (L1 â\89¡[h, o, T] L2 → ⊥) →
- â\88\83â\88\83L,L0. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] L & L1 â\89¡[h, o, T] L â\86\92 â\8a¥ & â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, T] L0 & L0 â\89¡[h, o, T] L2.
+lemma lfpxs_lfdneq_inv_step_sn: â\88\80h,o,G,L1,L2,T. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L2 â\86\92 (L1 â\89\9b[h, o, T] L2 → ⊥) →
+ â\88\83â\88\83L,L0. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] L & L1 â\89\9b[h, o, T] L â\86\92 â\8a¥ & â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, T] L0 & L0 â\89\9b[h, o, T] L2.