rw [TP_eq_iff]
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ¬ℓ = ℓ'
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') ↔ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ