proposition: Lemma f_g_subset B A : A <<= f B -> g A <<= B.
proof: Proof. revert B; induction A; intros B H; cbn. * firstorder. * assert (a el f B) by firstorder. unfold f in H0. eapply in_map_iff in H0 as ((x,y) & ? & ?). inv H0. intros ? [|]; subst. { cbn. now rewrite !f_g_s'_inv. } firstorder. Qed.
imports: List Lia Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions