simp [ofLen]
x y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := x } { index := y } n ∈ ofLen (x + y + n + 1)
x y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := x } { index := y } n ∈ Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (x + y + n)) ∨
    stmt { index := x } { index := y } n ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x_1 => Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x_1) (ofLen (x + y + n - ↑x_1))))
          (Finset.attach (Finset.range (x + y + n))) ∨
      stmt { index := x } { index := y } n ∈ baseProgram (x + y + n + 1)