| LetIn of string * term * term (* name, body, where *)
| LetRec of induction_kind * (string * term * term option * int) list * term
(* (name, body, type, decreasing argument) list, where *)
| LetIn of string * term * term (* name, body, where *)
| LetRec of induction_kind * (string * term * term option * int) list * term
(* (name, body, type, decreasing argument) list, where *)