proposition: Lemma FST_bunion_sub T a b c c' : FSTeq <<= T -> T ⊢ is_bunion a b c -> T ⊢ is_bunion a b c' -> T ⊢ c ⊆ c'.
proof: Proof. intros HT H1 H2. prv_all x. apply II. apply CE2 in H1. apply (AllE x) in H1. cbn in H1. subsimpl_in H1. rewrite imps in H1. apply (DE H1). - apply CE1, CE1 in H2. apply (AllE x) in H2. cbn in H2. subsimpl_in H2. eapply IE. apply (Weak H2); auto. auto. - apply CE1, CE2 in H2. apply (AllE x) in H2. cbn in H2. subsimpl_in H2. eapply IE. apply (Weak H2); 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)