Prove weakening for `typed`
Part of an answer to an Iris HelpDesk question — see https://mattermost.mpi-sws.org/iris/pl/m64hgftb8ffpmbdhnxkoo7ga8r.
Part of an answer to an Iris HelpDesk question — see https://mattermost.mpi-sws.org/iris/pl/m64hgftb8ffpmbdhnxkoo7ga8r.