proposition: Lemma BPCP_P : dPCPb R <-> exists n x, @i_atom _ _ _ (FIB n) P ((Vector.cons _ x _ (Vector.cons _ x _ (Vector.nil _)))).
proof: Proof. split. - intros [s H]. exists (|s|), (ienc s). cbn. now apply drv_cdrv'. - intros [n[ [ [s H]|] H'] ]. + cbn in H'. now exists s. + destruct H'. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation