constructor
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ (∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = τ) ∧ ¬evaluate M w τ
case h.left
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = τ

case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ¬evaluate M w τ