exists p
case h.h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ ∃
    x ∈
      (fun y a =>
          Acc.rec
            (fun x₁ h ih =>
              (fun a a_1 =>
                  (match (motive :=
                      (x : ℕ) →
                        ((y : ℕ) → (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                          Finset LoopProgram)
                      a with
                    | 0 => fun x => ∅
                    | Nat.succ n => fun x =>
                      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                          Finset.fold (fun x x_1 => x ∪ x_1) ∅
                            (fun x_1 =>
                              match x_1 with
                              | { val := l, property := h } =>
                                let_fun this := ⋯;
                                Finset.image
                                  (fun x =>
                                    match x with
                                    | (a, b) => concat a b)
                                  (Finset.product (x l ⋯) (x (n - l) ⋯)))
                            (Finset.attach (Finset.range n)) ∪
                        baseProgram (n + 1))
                    a_1)
                x₁ ih)
            ⋯)
        (Nat.add n 0) ⋯,
    p' ∈ extendLenOne x
no goals