This is proved via a lemma asserting that
a terminated tree rooted at null-literal
has leaves that satisfy null-literalp.
The lemma is proved by exhaustively opening abnf-tree-with-root-p,
thus prescribing the exact form of the tree,
and in particular its leaves.
The theorem is then proved by instantiating the lemma
to the witness tree of grammar-null-literalp.