proposition: Lemma b3_allowed : hsc [a_b_a] b3.
proof: Proof. pose ζ i := if i is 0 then bullet else if i is 1 then bullet else var i. have -> : b3 = substitute ζ a_b_a by done. apply: hsc_var. by left. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP