proposition: Lemma gamma_mono A B : A <<= gamma B -> gamma A <<= B.
proof: Proof. induction A as [ | (x,y) ]; cbn; intros. - firstorder. - intros ? [ <- | ]. + assert ( (x, y) el gamma B) by firstorder. unfold gamma in H0. eapply in_map_iff in H0 as ((x',y') & ? & ?). inv H0. now simpl_list. + firstorder. Qed.
imports: List Lia Undecidability.CFG.CFP Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions