proposition: Lemma encode_bool_injective {a b} : encode_bool a = encode_bool b -> a = b.
proof: Proof. case: a b; by case. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP