refine' .inr $ .inl (Finset.mem_fold_union_iff.mpr ⟨⟨a.len, _⟩, _⟩)
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)
case refine'_1
p a b : LoopProgram
⊢ len a ∈ Finset.range (len a + len b)

case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ?refine'_1 } ∈ 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 := ?refine'_1 })
          (ofLen (len a + len b - ↑{ val := len a, property := ?refine'_1 })))