Fix elab

Use option (id typeN) instead of empty strings.  Also add termination proof for
elab_p.