proposition: Lemma list_or_closed n A : (forall a, In a A -> bounded n a) -> bounded n (list_or A).
proof: Proof. intros H. induction A; solve_bounds. - apply H. now left. - apply IHA. intros a' Ha. apply H. now right. 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