add some more option_included lemmas

This came up while playing around with gmap_view: we can use Some x ≼ Some y to encode the reflexive closure of ≼, and that works much better than writing x ≼ y ∨ x ≡ y -- in particular if we have the right lemmas, such as the ones being added here.