simp_all only [List.mem_attach, forall_true_left, Subtype.forall, not_forall, evaluate, not_and]
case mpr
α : Program
ℓ ℓ' : TP α
ldiff : ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
W : Type
M : KripkeModel W
w : W
⊢ ¬evaluate M w (signature α ℓ⋀signature α ℓ')
case mpr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
ldiff : ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), ¬ℓ ⟨x, x_1⟩ = ℓ' ⟨x, x_1⟩
⊢ evaluate M w (signature α ℓ) → ¬evaluate M w (signature α ℓ')