-lemma after_inv_apply: â\88\80f2,f1,f,n2,n1,n. n2@f2 â\8a\9a n1@f1 â\89¡ n@f →
- (n2@f2)@â\9d´n1â\9dµ = n â\88§ (â\86\93*[n1]f2) â\8a\9a f1 â\89¡ f.
+lemma after_inv_apply: â\88\80f2,f1,f,n2,n1,n. n2@f2 â\8a\9a n1@f1 â\89\98 n@f →
+ (n2@f2)@â\9d´n1â\9dµ = n â\88§ (â\86\93*[n1]f2) â\8a\9a f1 â\89\98 f.