proposition: Lemma f_subset B A : A <<= B -> f A <<= f B.
proof: Proof. induction A in B |- *; intros H; cbn. * firstorder. * intros ? [| H0]; subst. - unfold f. eapply in_map_iff. exists a. constructor; eauto. apply H; simpl; auto. - eapply IHA in H0; eauto. intros ? ?; apply H; simpl; auto. Qed.
imports: List Lia Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions