Please check the code in ex1, why “destruct H” fail? what’s the meaning of this error message?

```
(* the hypothesis is "or" and the conclusion is "sumbool" *)
Example ex1 : forall m : nat, (m = 1 \/ m = 2) -> {m = 1} + {m = 2}.
Proof.
intros.
Fail destruct H.
(* Case analysis on sort Set is not allowed for inductive definition or. *)
(* why failed here? *)
Abort.
(* the hypothesis is "or" and the conclusion is a simple prop *)
Example ex2 : forall m : nat, (m = 1 \/ m = 2) -> m >= 1.
Proof.
intros.
destruct H. (* it's OK *)
Admitted.
(* the hypothesis is "and" and the conclusion is "sumbool" *)
Example ex3 : forall m : nat, 1 <= m <= 2 -> {m = 1} + {m = 2}.
Proof.
intros.
destruct H. (* it's OK *)
Admitted.
```