-lemma aaa_inv_lifts: â\88\80G,L2,T2,A. â¦\83G, L2â¦\84 â\8a¢ T2 â\81\9d A â\86\92 â\88\80b,f,L1. â¬\87*[b, f] L2 â\89¡ L1 →
- â\88\80T1. â¬\86*[f] T1 â\89¡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A.
+lemma aaa_inv_lifts: â\88\80G,L2,T2,A. â¦\83G, L2â¦\84 â\8a¢ T2 â\81\9d A â\86\92 â\88\80b,f,L1. â¬\87*[b, f] L2 â\89\98 L1 →
+ â\88\80T1. â¬\86*[f] T1 â\89\98 T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A.