simp
case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ⋯ } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ⋯ })
          (ofLen (len a + len b - ↑{ val := len a, property := ⋯ })))
case refine'_2
p a b : LoopProgram
⊢ (a, b) ∈ Finset.product (ofLen (len a)) (ofLen (len b))