proposition: Lemma derivable_derivations B s t : derivable B s t -> exists n, (s, t) el derivations B n.
proof: Proof. induction 1. - exists 0. apply H. - destruct IHderivable as [n Hn]. exists (S n). apply in_flat_map. exists (x, y). split; trivial. apply in_map_iff. exists (u,v). cbn. split; trivial. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets.ZF Lia Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)