proposition: Lemma M_bunion_unique a b c c' : M_is_bunion a b c -> M_is_bunion a b c' -> c = c'.
proof: Proof. Proof using M_FST VIEQ. intros H1 H2. apply M_ext; firstorder. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.FST Undecidability.FOL.Sets.FST Lia Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)