simp_all [TP, contradiction, signature_iff]
case mp
α : Program
ℓ ℓ' : TP α
contrasign : contradiction (signature α ℓ⋀signature α ℓ')
⊢ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
case mp
α : Program
ℓ ℓ' : TP α
contrasign :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    (∀ (a : Formula) (b : a ∈ testsOfProgram α), ℓ ⟨a, b⟩ = true ↔ evaluate M w a) →
      ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), ¬(ℓ' ⟨x, x_1⟩ = true ↔ evaluate M w x)
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), ¬ℓ ⟨x, x_1⟩ = ℓ' ⟨x, x_1⟩