simp [len_gt_zero]
case refine'_1
p a b : LoopProgram
⊢ len a < len a + len b

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
⊢ { 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 := ⋯ })))