Parsing failure propagation theorems for the parser of ABNF grammars.
If certain parsing functions fail, other parsing functions fail as well, because the former parse prefixes of the latter. In other words, parsing failures ``propagate''.
The parsing failure propagation theorems below state this kind of facts. These theorems are used as rewrite rules in the completeness theorems and in the disambiguation theorems. The parsing failure propagation theorems are disabled by default; they are enabled in the completeness and disambiguation theorems that use them.