apply Finset.mem_union_right
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := 0 } p ∈
    WellFounded.fix ofLen.proof_1
      (fun a a_1 =>
        (match (motive :=
            (x : ℕ) →
              ((y : ℕ) → (invImage (fun a => 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 => Finset.image (fun x => concat x.1 x.2) (Finset.product (x ↑x_1 ⋯) (x (n - ↑x_1) ⋯)))
                  (Finset.attach (Finset.range n)) ∪
              match n + 1 with
              | 0 => ∅
              | 1 => lenOne
              | 2 => Finset.image (loop { index := 0 }) lenOne
              | x => ∅)
          a_1)
      (1 + 1)
case h
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := 0 } p ∈
    match 1 + 1 with
    | 0 => ∅
    | 1 => lenOne
    | 2 => Finset.image (loop { index := 0 }) lenOne
    | x => ∅