proposition: Fact h10luc_sem_dec l φ : { c | In c l /\ ~ ⟪c⟫ φ } + { forall c, In c l -> ⟪c⟫ φ }.
proof: Proof. apply list_choose_dep. intros c _; apply plus_swap. destruct c as ((?,?),?); apply eq_nat_dec. Qed.
imports: List Arith Undecidability.Shared.Libs.DLW.Utils(utils_decidable utils_nat) Undecidability.DiophantineConstraints(H10C)