Theorem: boxHelperTermination (Pdl/Unfold.lean)

State before:
n : ℕ
a γ : Program
ℓ : TP γ
ψ : Formula
⊢ (∀ δ ∈ P γ ℓ,
      (∀ α ∈ δ, α ∈ subprograms γ) ∧
        (∀ (h : δ.length > 0), isAtomic (δ.get (Fin.ofNat' 0 h)) = true) ∧
          ∀ iα ∈ δ.enum, iα.2 = γ ↔ isAtomic γ = true ∧ iα.1 = n ∧ iα.1 = 1 ∨ isStar γ = true ∧ iα.1 = n) ∧
    ∀ φ ∈ (unfoldBox γ ψ).join,
      φ ∈ fischerLadner (⌈γ⌉ψ) ∧
        (φ = ψ ∨ (∃ τ ∈ testsOfProgram γ, φ = (~τ)) ∨ ∃ δ, (φ = ⌈a⌉⌈⌈δ⌉⌉ψ) ∧ ∀ α ∈ δ, α ∈ subprograms γ)
Tactic:
sorry
State after:
no goals