Comment by 082349872349872

A cursory search reveals they're not builtin, but were written for the talk: https://github.com/awalterschulze/ccc-talk/blob/main/Coq/src...

    nail ~= intros
    wat ~= discriminate
    etc.