proposition: Lemma FST_enc_stack_app T A B : FSTeq <<= T -> T ⊢ is_bunion (enc_stack A) (enc_stack B) (enc_stack (A ++ B)).
proof: Proof. intros HT. induction A as [|[s t] A IH]; cbn. - apply CI. apply CI. + prv_all x. apply II, Exp. apply imps. apply FST_eset'. auto. + prv_all x. apply II, Ctx. auto. + prv_all x. apply II, DI2, Ctx. auto. - apply CI. apply CI. + prv_all x. apply II. assert1 H. apply FST_adj in H; auto. apply FST_adj; auto. apply (DE H); clear H. * apply DI1. auto. * apply DI2. repeat apply CE1 in IH. apply (AllE x) in IH. cbn in IH. subsimpl_in IH. eapply IE. apply (Weak IH). auto. auto. + prv_all x. apply II. apply FST_adj; auto. apply DI2. apply CE1, CE2 in IH. apply (AllE x) in IH. cbn in IH. subsimpl_in IH. eapply IE. apply (Weak IH). auto. auto. + prv_all x. apply II. assert1 H. apply FST_adj in H; auto. apply (DE H); clear H. * apply DI1. apply FST_adj; auto. * apply CE2 in IH. apply (AllE x) in IH. cbn in IH. subsimpl_in IH. eapply DE. eapply IE. apply (Weak IH); auto. auto. 2: auto. apply DI1. apply FST_adj; 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)