finish rev. just needed to induct and rewrite. nice, but do we *have* to use the snoc definition?