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 M_ZF. intros HS HO Hf Hk HX Hp. destruct (HS k HO) as [n Hn]. change (k ≡' numeral n) in Hn. rewrite Hn in Hk. rewrite Hn in HX. 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'&Hp). 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) Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_ZF Lia Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation) Morphisms