Inductive exp : Set :=
  | Const : nat -> exp
  | Plus : exp -> exp -> exp
  | Times : exp -> exp -> exp.

Inductive eval : exp -> nat -> Prop :=
  | evalConst : forall (n:nat),
    eval (Const n) n
  | evalPlus : forall (e1 e2:exp) (n1 n2:nat),
    eval e1 n1
    -> eval e2 n2
    -> eval (Plus e1 e2) (n1 + n2)
  | evalTimes : forall (e1 e2:exp) (n1 n2:nat),
    eval e1 n1
    -> eval e2 n2
    -> eval (Times e1 e2) (n1 * n2).

Theorem total : forall (e:exp), {n:nat | eval e n}.
induction e.
exists n.
apply evalConst.
destruct IHe1.
destruct IHe2.
exists (x + x0).
apply evalPlus.
trivial.
trivial.
destruct IHe1.
destruct IHe2.
exists (x * x0).
apply evalTimes.
trivial.
trivial.
Qed.