proposition: Lemma bitstring_false a : ~ false el to_bitstring a.
proof: Proof. induction a; cbn; firstorder congruence. Qed.
imports: List Lia Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions