proposition: Lemma ZF_derivations_bound T B k n x : ZFeq' <<= T -> T ⊢ opair k x ∈ enc_derivations B n -> T ⊢ k ∈ σ (tnumeral n).
proof: Proof. induction n in T |- *; cbn; intros HT H. - apply ZF_sing_iff in H; trivial. eapply ZF_eq_elem; trivial. apply ZF_sym'; trivial. eapply opair_inj1; trivial. apply H. apply ZF_refl'; trivial. eapply ZF_bunion_el'; trivial. apply DI2. apply ZF_sing_iff; trivial. apply ZF_refl'; trivial. - apply ZF_bunion_inv in H; trivial. apply (DE H). + apply ZF_bunion_el1. auto. apply IHn; auto. + apply ZF_bunion_el2. auto. apply ZF_sing_iff. auto. eapply opair_inj1. auto. apply ZF_sing_iff; auto. Qed.
imports: Undecidability.FOL.ZF Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Sets.ZF Undecidability.FOL.Reductions.PCPb_to_ZF Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)