proposition: Lemma enc_derivations_functional B n x y y' : ZFeq' ⊢ opair x y ∈ enc_derivations B n → opair x y' ∈ enc_derivations B n → y ≡ y'.
proof: Proof. induction n; cbn -[derivations]. - repeat apply II. eapply opair_inj2. auto. eapply ZF_trans'. auto. + apply ZF_sing_iff; auto. + apply ZF_sym'. auto. apply ZF_sing_iff; auto. - apply bunion_use; try apply bunion_use. 1,2,5: auto. + repeat rewrite <- imps. now apply (Weak IHn). + apply Exp. eapply IE. apply (@ZF_numeral_wf _ (S n)). auto. eapply ZF_derivations_bound. auto. eapply ZF_eq_elem. auto. 2: apply ZF_refl'; auto. 2: auto. apply ZF_eq_opair; auto. eapply opair_inj1; auto. apply ZF_refl'. auto. + apply Exp. eapply IE. apply (@ZF_numeral_wf _ (S n)). auto. eapply ZF_derivations_bound. auto. eapply ZF_eq_elem. auto. 2: apply ZF_refl'; auto. 2: auto. apply ZF_eq_opair; auto. eapply opair_inj1; auto. apply ZF_refl'. auto. + eapply opair_inj2. auto. eapply ZF_trans'; auto. apply ZF_sym'; 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)