cases' h_stmt with h h <;> rw [h] <;> rfl
case zero.zero.zero
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ len (stmt { index := Nat.zero } { index := Nat.zero } Nat.zero) = 1
no goals