¿Cómo se producen tipos (o teoremas) a partir de términos de prueba (programas u objetos) en Coq?

Tenía curiosidad por aprender sobre la inferencia de tipos en Coq. Quería una forma concreta en Coq de generar tipos (teoremas) dados un término/objeto/programa de prueba. Entonces, dado un término de prueba (quizás con un agujero, quizás sin agujeros o quizás un sub-término de prueba), ¿puedo generar su tipo de manera determinista? Me preguntaba si Coq nos proporciona esta funcionalidad para esto
por ejemplo, en pseudo-Coq:

program := (fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n)
.

type := Coq.Proofterm2.Type(program).

Print type.

¿Cuál es la función correcta en Coq para hacer eso: Dado un término de prueba, obtén su tipo (inferencia de tipos, básicamente, en Coq/Gallina)?

Estaba jugando con esta prueba y sus objetos de prueba:

Theorem add_easy_induct_1:
    forall n:nat,
      n + 0 = n.
  Proof.
    Show Proof.
    intros.
    Show Proof.
    induction n as [| n' IH].
    Show Proof.
    - simpl. reflexivity.
    Show Proof.
    - simpl. rewrite -> IH. reflexivity.
    Show Proof.
  Qed.

Algunos ejemplos de salida:

?Goal
(fun n : nat => ?Goal)
(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) ?Goal
  (fun (n' : nat) (IH : n' + 0 = n') => ?Goal0) n)
(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') => ?Goal) n)
(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n)
add_easy_induct_1 = 
fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n
     : forall n : nat, n + 0 = n

Arguments add_easy_induct_1 _%nat scope

Usé el jsCoq, que es realmente útil mientras espero a que se instale Coq, Opam, etc. en mi nuevo ordenador.