Make the inverse of functor_forall transparent

If being able to step through the proofs in proviola is preferred, I can instead stuff this in a section and make separate lemmas for the proofs.