-fact aaa_inv_abst_aux: â\88\80G,L,T,A. â¦\83G,Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â\88\80p,W,U. T = â\93\9b{p}W.U →
- â\88\83â\88\83B1,B2. â¦\83G,Lâ¦\84 â\8a¢ W â\81\9d B1 & â¦\83G,L.â\93\9bWâ¦\84 ⊢ U ⁝ B2 & A = ②B1.B2.
+fact aaa_inv_abst_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© â\8a¢ T â\81\9d A â\86\92 â\88\80p,W,U. T = â\93\9b[p]W.U →
+ â\88\83â\88\83B1,B2. â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d B1 & â\9d¨G,L.â\93\9bWâ\9d© ⊢ U ⁝ B2 & A = ②B1.B2.