proposition: Lemma tau2_bin_map {A : list (list nat * list nat)} : tau2 (bin_map A) = bin (tau2 A).
proof: Proof. elim: A; first done. move=> [x y] A IH /=. by rewrite bin_appP IH. Qed.
imports: List Undecidability.PCP.PCP Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun