-lemma after_inv_pxx: â\88\80g1,g2,g. g1 â\8a\9a g2 â\89\98 g â\86\92 â\88\80f1. â\86\91f1 = g1 →
- (â\88\83â\88\83f2,f. f1 â\8a\9a f2 â\89\98 f & â\86\91f2 = g2 & â\86\91f = g) ∨
- (â\88\83â\88\83f2,f. f1 â\8a\9a f2 â\89\98 f & ⫯f2 = g2 & ⫯f = g).
+lemma after_inv_pxx: â\88\80g1,g2,g. g1 â\8a\9a g2 â\89\98 g â\86\92 â\88\80f1. ⫯f1 = g1 →
+ (â\88\83â\88\83f2,f. f1 â\8a\9a f2 â\89\98 f & ⫯f2 = g2 & ⫯f = g) ∨
+ (â\88\83â\88\83f2,f. f1 â\8a\9a f2 â\89\98 f & â\86\91f2 = g2 & â\86\91f = g).