proposition: Lemma adequate0E {v w P} : not (adequate v w P 0).
proof: Proof. by move=> [? [?]] /derE. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP