proposition: Lemma g_s'_app n x y : g_s' (f_s x ++ y) n = match x with nil => g_s' y n | m :: x => n + m :: x ++ g_s' y 0 end.
proof: Proof. revert n y. induction x as [ | m]; intros; cbn in *. - reflexivity. - revert n; induction m; intros; cbn in *. + destruct x. * do 2 f_equal. lia. * rewrite IHx. f_equal. lia. + rewrite IHm. f_equal. lia. Qed.
imports: List Lia Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions