(* PG accepts this as valid though it isn't;
   see http://proofgeneral.inf.ed.ac.uk/trac/ticket/296 *)
Check nat.&!&*\:,.:<*&!)@)$.