proposition: Fact h10c_sem_dec c φ : {〚c〛φ } + { ~〚c〛φ }.
proof: Proof. destruct c; apply eq_nat_dec. Qed.
imports: List Arith Undecidability.Shared.Libs.DLW.Utils(utils_decidable utils_nat) Undecidability.DiophantineConstraints(H10C)