Theorem rev-r

• Type: An axiom
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: rev-app, rev-disjoint, rev-dups, rev-empty, rev-in, rev-length, rev-mklist, rev-one, rev-rest, rev-rev-identity,
• Used by units in proved state: list-del, list-perm,
• Proof exists?: No