proposition: Lemma eq_binP {x y} : x = y <-> (bin x) = (bin y).
proof: Proof. elim: x y; first by case. move=> a x IH [|b y /=]; first done. constructor; first by move=> [<- <-]. case. elim: a b. { case; last done. by move=> [/IH ->]. } move=> a IH2 [|b /=]; first done. by move=> [/IH2 [<- <-]]. Qed.
imports: List Undecidability.PCP.PCP Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun