intro contrasign
case mp
α : Program
ℓ ℓ' : TP α
⊢ contradiction (signature α ℓ⋀signature α ℓ') → ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ
case mp
α : Program
ℓ ℓ' : TP α
contrasign : contradiction (signature α ℓ⋀signature α ℓ')
⊢ ¬∀ τ ∈ (testsOfProgram α).attach, ℓ τ = ℓ' τ