proposition: Lemma enc_derivations_functional B n x y y' : FSTeq ⊢ 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 FST_trans'. auto. + apply FST_sing_iff; auto. + apply FST_sym'. auto. apply FST_sing_iff; auto. - apply II. assert1 H1. apply FST_adj in H1; auto. apply (DE H1). all: apply II; assert1 H2; apply FST_adj in H2; auto; apply (DE H2). + eapply opair_inj2. auto. eapply FST_trans'; auto. apply FST_sym'; auto. + apply Exp. eapply IE. apply (@FST_numeral_wf _ (S n)). auto. eapply FST_derivations_bound. auto. eapply FST_eq_elem. auto. 2: apply FST_refl'; auto. 2: auto. apply FST_eq_opair; auto. eapply opair_inj1; auto. apply FST_refl'. auto. + apply Exp. eapply IE. apply (@FST_numeral_wf _ (S n)). auto. eapply FST_derivations_bound. auto. eapply FST_eq_elem. auto. 2: apply FST_refl'; auto. 2: auto. apply FST_eq_opair; auto. eapply opair_inj1; auto. apply FST_refl'. auto. + repeat rewrite imps in IHn. apply (Weak IHn). auto 8. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Sets.FST Undecidability.FOL.FST Undecidability.FOL.Reductions.PCPb_to_FST Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)