apply Finset.mem_product.mpr
case refine'_2
p a b : LoopProgram
⊢ (a, b) ∈ Finset.product (ofLen (len a)) (ofLen (len b))
case refine'_2
p a b : LoopProgram
⊢ (a, b).1 ∈ ofLen (len a) ∧ (a, b).2 ∈ ofLen (len b)