-lemma sor_inv_xxn: â\88\80g1,g2,g. g1 â\8b\93 g2 â\89¡ g → ∀f. ⫯f = g →
- â\88¨â\88¨ â\88\83â\88\83f1,f2. f1 â\8b\93 f2 â\89¡ f & ⫯f1 = g1 & ↑f2 = g2
- | â\88\83â\88\83f1,f2. f1 â\8b\93 f2 â\89¡ f & ↑f1 = g1 & ⫯f2 = g2
- | â\88\83â\88\83f1,f2. f1 â\8b\93 f2 â\89¡ f & ⫯f1 = g1 & ⫯f2 = g2.
+lemma sor_inv_xxn: â\88\80g1,g2,g. g1 â\8b\93 g2 â\89\98 g → ∀f. ⫯f = g →
+ â\88¨â\88¨ â\88\83â\88\83f1,f2. f1 â\8b\93 f2 â\89\98 f & ⫯f1 = g1 & ↑f2 = g2
+ | â\88\83â\88\83f1,f2. f1 â\8b\93 f2 â\89\98 f & ↑f1 = g1 & ⫯f2 = g2
+ | â\88\83â\88\83f1,f2. f1 â\8b\93 f2 â\89\98 f & ⫯f1 = g1 & ⫯f2 = g2.