get recover to type-check
get recover to type-check

something seems off in the recover_ok proof; probably some
unification happening too early.

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl