naive_solver does not solve trivial inconsistencies involving is_Some
Example ex1 : is_Some (None : option nat) → False.
Proof.
Fail naive_solver. (* No matching clauses for match. *)
unfold is_Some. naive_solver. (* No more goals. *)
Qed.
Example ex2 : is_Some (Some 10).
Proof.
naive_solver. (* No more goals. *)
Qed.