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