proposition: Lemma append_all_el T B s t x y : FSTeq <<= T -> T ⊢ opair x y ∈ enc_stack B -> T ⊢ opair (prep_string s x) (prep_string t y) ∈ enc_stack (append_all B (s/t)).
proof: Proof. intros HT H. induction B as [|[u v] B IH] in T, HT, H |- *; cbn in *. - apply Exp. eapply IE. 2: apply H. now apply FST_eset'. - eapply FST_adj; trivial. apply FST_adj in H; trivial. eapply (DE H). + assert1 H'. apply FST_sing_iff in H'; try now auto. apply DI1. auto. rewrite !prep_string_app. apply FST_eq_opair. auto. * apply FST_eq_prep. auto. eapply opair_inj1; eauto. * apply FST_eq_prep. auto. eapply opair_inj2; eauto. + apply DI2. apply IH; 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)