fact: Fixpoint f_s (x : string nat) : string bool := match x with | nil => nil | a :: x => to_bitstring a ++ [false] ++ f_s x end.
imports: List Lia Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions