Theorem: LoopProgram.len_gt_zero (FormalSystems/Computability/Loop.lean)

State before:
⊢ ∀ (p : LoopProgram), len p > 0
Tactic:
intro p
State after:
p : LoopProgram
⊢ len p > 0

State before:
p : LoopProgram
⊢ len p > 0
Tactic:
cases p <;> unfold len <;> simp_arith
State after:
no goals