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