proposition: Lemma soundness {v w P} : MPCPb ((v, w), P) -> hsc (Γ v w P) a_b_a.
proof: Proof. move=> [A [/soundness_ind + H]] => /(_ _ _ H){H} ?. apply: hsc_arr; last eassumption. pose ζ i := var i. have Hζ: forall s, s = substitute ζ s. { elim; first done. by move=> ? + ? /= => <- <-. } rewrite (Hζ (arr _ _)). apply: hsc_var. rewrite /Γ. right. by left. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP