Reverse


THEOREM    rev (rev xs) = xs
rev_rev_ident: rev (rev ?xs) = ?xs

Proof unavailable