proposition: Lemma f_g_s'_inv x : g_s (f_s x) = x.
proof: Proof. unfold g_s. setoid_rewrite <- app_nil_r at 2. rewrite g_s'_app. destruct x; eauto. cbn. now rewrite app_nil_r. Qed.
imports: List Lia Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions