proposition: Lemma gamma1_spec B C : B <<= gamma1 C -> exists A, A <<= C /\ gamma1 A = B.
proof: Proof. induction B as [ | (x,y)]; cbn; intros. - eauto. - assert ((x, y) el gamma1 C) by firstorder. unfold gamma1 in H0. eapply in_map_iff in H0 as ((x',y') & ? & ?). inv H0. assert (B <<= gamma1 C) as (A & Hi & He) % IHB by firstorder. exists ((x, y') :: A). split. + auto with datatypes. + now subst. Qed.
imports: List Lia Undecidability.CFG.CFP Undecidability.CFG.Util.Facts Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions