cases p <;> simp [len] at h <;> simp [h, lenOne, Variable.eq]
p : LoopProgram
h : len p = 1
⊢ p ∈ lenOne
case concat
p₁✝ p₂✝ : LoopProgram
h : len p₁✝ = 0 ∧ len p₂✝ = 0
⊢ False

case loop
x✝ : Variable
p✝ : LoopProgram
h : len p✝ = 0 ∧ x✝.index = 0
⊢ False