proposition: Lemma Γ_allowed {v w P} : forall r, In r (Γ v w P) -> hsc [a_b_a] r.
proof: Proof. apply /Forall_forall. constructor; [|constructor; [|constructor]]. - do 3 (apply: arr_allowed). by apply: b3_allowed. - apply: arr_allowed. have -> : a_b_a = substitute var a_b_a by done. apply: hsc_var. by left. - do 4 (apply: arr_allowed). by apply: b3_allowed. - apply /Forall_forall => ? /in_map_iff [[x y]] [<- _]. do 4 (apply: arr_allowed). by apply: b3_allowed. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP