Coq definitions: Prop or Set?

[liyishuai]

From the untyped lambda calculus example, suppose I want to compute whether a reduction is beta:

Definition is_beta {t t' : term} (r : reduce t t') : bool :=
  match r with
  | ax_app _ _ _ _ => true
  | _ => false
  end.

Coq complains that:

Error:
Incorrect elimination of "r" in the inductive type "reduce":
the return type has sort "Set" while it should be "Prop".
Elimination of an inductive object of sort Prop is not allowed on a predicate in sort Set
because proofs can be eliminated only to build proofs.

Is there a specific reason to represent definitions with Prop rather than Set?