proposition: Lemma bin_appP {x y} : bin (x ++ y) = bin x ++ bin y.
proof: Proof. by rewrite /bin ? flat_map_concat_map map_app concat_app. Qed.
imports: List Undecidability.PCP.PCP Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun