specialize ℓ_conform (~τ) τ τ_in
case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ) → evaluate M w (~τ)
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x