proposition: Lemma M_solutions_el B f k X p : standard M -> k ∈ ω -> M_function f -> M_solutions B f k -> M_opair k X ∈ f -> p ∈ X -> exists u v, p = M_enc_card u v /\ derivable B u v.
proof: Proof. Proof using VIEQ M_ZF. intros HS HO Hf Hk HX Hp. destruct (HS k HO) as [n -> % VIEQ]. pose proof (H := solutions_derivations Hk (le_n n)). rewrite (Hf _ _ _ HX H) in Hp. apply enc_stack_el' in Hp as (s&t&H'&->). exists s, t. split; trivial. eapply derivations_derivable; eauto. 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)