∀ (s : String) (p : s.Pos) (res : Lean.Name) (n : ℕ) (h : ¬p = s.endPos) (h_1 : ¬p.next h = s.endPos),
  (invImage
        (fun x =>
          PSum.casesOn x (fun _x => PSigma.casesOn _x fun p res => PSigma.casesOn res fun res n => p) fun _x =>
            PSum.casesOn _x (fun _x => PSigma.casesOn _x fun p res => p) fun _x =>
              PSigma.casesOn _x fun p₀ res => PSigma.casesOn res fun res acc => PSigma.casesOn acc fun acc ucount => p₀)
        String.Pos.instWellFoundedRelation).1
    (PSum.inr (PSum.inl ⟨(p.next h).next h_1, res.num n⟩)) (PSum.inl ⟨p, ⟨res, n⟩⟩)