fact: Definition f (P : stack bool) (A : stack bool) := omap (fun x => pos card_eq x P) A.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.Definitions