forall_arithmetic_facts(ok).