cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)
no goals