proposition: Lemma combinations_step B n (i x y : term) : FSTeq ⊢ i ∈ tnumeral n → opair i x ∈ enc_derivations B n → combinations B x y → opair (σ i) y ∈ enc_derivations B n.
proof: Proof. induction n; cbn. - apply II. apply Exp. apply imps. apply FST_eset. - 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). + apply Exp. eapply IE. apply (FST_numeral_wf n). auto. eapply FST_eq_elem. auto. apply FST_refl'. auto. eapply FST_trans'. auto. apply FST_sym'. auto. eapply opair_inj1. auto. auto. auto. apply FST_sig_el. auto. + apply II. apply FST_adj. auto 8. apply DI1. apply FST_eq_opair. auto 8. * apply FST_eq_sig; auto 8. * eapply combinations_eq; auto 8. apply enc_derivations_eq. auto 8. eapply FST_eq_elem; auto 8; try apply FST_refl'; auto 8. eapply FST_eq_opair; auto 8; try apply FST_refl'. auto 8. + apply Exp. eapply IE. apply (FST_numeral_wf (S n)). auto. eapply FST_eq_elem. auto. eapply opair_inj1. auto. auto. apply FST_refl'. auto. cbn. apply FST_adj. auto. apply DI2. auto. + apply II. apply FST_adj. auto 8. apply DI2. eapply IE. eapply IE. eapply IE. * eapply Weak. apply IHn. auto 8. * auto. * auto. * auto. 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)