∀ {F : PFunctor.{uA, uB}} {n : ℕ} (x : PFunctor.Approx.CofixA F n.succ) (y : PFunctor.Approx.CofixA F (n.succ + 1))
  {i : F.B (PFunctor.Approx.head' x)} {j : F.B (PFunctor.Approx.head' y)},
  i ≍ j →
    PFunctor.Approx.Agree x y → PFunctor.Approx.Agree (PFunctor.Approx.children' x i) (PFunctor.Approx.children' y j)