proposition: Lemma tau1_f A : tau1 (f A) = f_s (tau1 A).
proof: Proof. induction A as [ | (x,y) ]; cbn. - reflexivity. - unfold f in IHA. now rewrite IHA, f_s_app. Qed.
imports: List Lia Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic.Definitions