proposition: Lemma debin {A: list (list bool * list bool)} {P : list (list nat * list nat)} : incl A (bin_map P) -> exists B, A = bin_map B /\ incl B P.
proof: Proof. elim: A. { move=> *. exists []. by constructor. } move=> a A IH /incl_consE [+ +]. move /(@in_map_iff) => [[x' y'] [<- ?]]. move /IH => [B [-> HB]]. exists ((x', y') :: B). constructor; first done. by move=> ? [<- | /HB]. Qed.
imports: List Undecidability.PCP.PCP Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun