aesop
case mp.inr
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
w_ℓ : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ) → evaluate M w (~τ)
⊢ ℓ ⟨τ, τ_in⟩ = true ↔ evaluate M w τ
no goals