option_Forall predicate

Endorsed by @jung ("I think having such a predicate would make sense"), and by @robbertkrebbers ("+1 for option_Forall") in the iris mattermost.

• from_option lemmas:
  • from_option_fmap
  • from_option_proper_leibniz
  • option_Forall
  • option_Forall_proper
  • option_Forall_fmap
  • option_Forall_true
  • option_Forall_impl_strong_1
  • option_Forall_impl_strong_2
  • option_Forall_impl_strong_iff
  • option_Forall_impl
  • option_Forall_iff_strong_iff
  • option_Forall_iff
  • option_Forall_conj_strong