+ if not toplevel then F.fprintf f "(";
+ F.fprintf f "@[<hov 1>";
+ F.fprintf f "let %s:@;" name;
+ aux ~toplevel:true ctx ty;
+ F.fprintf f "@;≝ ";
+ aux ~toplevel:true ctx t;
+ F.fprintf f "@;in@;";
+ (aux ~toplevel (name::ctx) b);
+ F.fprintf f "@]";
+ if not toplevel then F.fprintf f ")";