simp [len, ofLen]
p a b : LoopProgram
⊢ concat a b ∈ ofLen (len (concat a b))
p a b : LoopProgram
⊢ concat a b ∈ Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (len a + len b)) ∨
    concat a b ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x => Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x) (ofLen (len a + len b - ↑x))))
          (Finset.attach (Finset.range (len a + len b))) ∨
      concat a b ∈ baseProgram (len a + len b + 1)