Require Export Coq.Numbers.Natural.Peano.NPeano.
Definition my_function: nat -> nat.
Proof.
  intros n. apply (S (S n)).
Qed.

(* how to find out what the result of (my_function 5) is? *)
(* the following line does not give any information: *)
Eval compute in (my_function 5). (* prints: = my_function 5 : nat *)

(* I would be interested in some output like: *)
Eval compute in (S (S 5)). (* prints: = 7 : nat *)