simp_all
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ (if ℓ' ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ)
no goals