proposition: Lemma tau2_g A B : A <<= f B -> tau2 (g A) = g_s (tau2 A).
proof: Proof. induction A as [ | (x,y)]; cbn. - reflexivity. - unfold g in IHA. intros. rewrite !IHA. { assert ( (x, y) el map f_c B) as ((x',y') & ? & ?) % in_map_iff by firstorder; inv H0. rewrite g_s'_app. destruct y'. + cbn. reflexivity. + rewrite f_g_s'_inv. cbn. reflexivity. } firstorder. Qed.
imports: List Lia Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions