simp_all
case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfProgram γ < 2 + lengthOfFormula τ
no goals