| LetIn of loc * 'term * 'ident
(* | Named_intros of loc * 'ident list (* joined with Intros above *) *)
(* | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *)
| LetIn of loc * 'term * 'ident
(* | Named_intros of loc * 'ident list (* joined with Intros above *) *)
(* | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *)