-lemma compose_inv_S2: â\88\80f2,f1,f,n2,n1,n. (n2@f2)â\88\98(⫯n1@f1) = n@f →
- ⫯(n2+f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+lemma compose_inv_S2: â\88\80f2,f1,f,n2,n1,n. (n2@f2)â\88\98(â\86\91n1@f1) = n@f →
+ â\86\91(n2+f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.