proposition: Lemma arr_allowed {s t} : hsc [a_b_a] t -> hsc [a_b_a] (arr s t).
proof: Proof. move=> H. apply: hsc_arr; last by eassumption. pose ζ i := if i is 0 then t else if i is 1 then s else var i. have -> : arr t (arr s t) = 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