-lemma cocompose_inv_pnx: â\88\80f2,f1,f,n1,x. (â\86\91f2) ~â\88\98 ((⫯n1)@f1) = x@f →
- â\88\83â\88\83n. ⫯n = x & f2 ~â\88\98 (n1@f1) = n@f.
+lemma cocompose_inv_pnx: â\88\80f2,f1,f,n1,x. (⫯f2) ~â\88\98 (â\86\91n1⨮f1) = x⨮f →
+ â\88\83â\88\83n. â\86\91n = x & f2 ~â\88\98 (n1⨮f1) = n⨮f.