∀ {α : Type} (env : Lean.Environment) (constantsPerTask : ℕ) (ngen : Lean.NameGenerator)
  (tasks : Array (Task (Lean.Meta.RefinedDiscrTree.InitResults✝ α))) (start cnt idx : ℕ),
  idx < env.header.moduleData.size →
    ∀ (ngen_1 : Lean.NameGenerator) (t : Task (Lean.Meta.RefinedDiscrTree.InitResults✝¹ α)),
      InvImage (fun x1 x2 => x1 < x2)
        (fun x =>
          PSigma.casesOn x fun ngen tasks =>
            PSigma.casesOn tasks fun tasks start =>
              PSigma.casesOn start fun start cnt => PSigma.casesOn cnt fun cnt idx => env.header.moduleData.size - idx)
        ⟨ngen_1, ⟨tasks.push t, ⟨idx + 1, ⟨0, idx + 1⟩⟩⟩⟩ ⟨ngen, ⟨tasks, ⟨start, ⟨cnt, idx⟩⟩⟩⟩