proposition: Lemma encode_list_injective {x y} : encode_list encode_bool x = encode_list encode_bool y -> x = y.
proof: Proof. elim: x y=> [|a x IH]; case=> //=. by move=> b y [] /encode_bool_injective => <- /IH <-. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP