some undocumented features i found while looking through the source code of the proof language beluga.