-lemma pr_nat_inv_succ_dx (f) (l1) (l2): @â\86\91â\9dªl1,fâ\9d« ≘ l2 → ∀k2. ↑k2 = l2 →
- â\88¨â\88¨ â\88\83â\88\83g,k1. @â\86\91â\9dªk1,gâ\9d« ≘ k2 & ↑k1 = l1 & ⫯g = f
- | â\88\83â\88\83g. @â\86\91â\9dªl1,gâ\9d« ≘ k2 & ↑g = f.
+lemma pr_nat_inv_succ_dx (f) (l1) (l2): @â\86\91â\9d¨l1,fâ\9d© ≘ l2 → ∀k2. ↑k2 = l2 →
+ â\88¨â\88¨ â\88\83â\88\83g,k1. @â\86\91â\9d¨k1,gâ\9d© ≘ k2 & ↑k1 = l1 & ⫯g = f
+ | â\88\83â\88\83g. @â\86\91â\9d¨l1,gâ\9d© ≘ k2 & ↑g = f.