proposition: Lemma list_or_spec A D (I : interp D) rho : rho ⊨ list_or A <-> exists phi, phi el A /\ rho ⊨ phi.
proof: Proof. induction A; cbn; split; auto. - firstorder. - intros [H|H]. + exists a. tauto. + apply IHA in H as [phi[H1 H2]]. exists phi. tauto. - intros [phi [[->|H1] H]]; auto. right. apply IHA. now exists phi. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation