proposition: Lemma f_s_app x y : f_s (x ++ y) = f_s x ++ f_s y.
proof: Proof. induction x; cbn. - reflexivity. - rewrite IHx. now rewrite <- app_assoc. Qed.
imports: List Lia Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions