make it so that we can give the option type (instead of the list of variants) to the type_sum lemmas

also update Iris

It is still not as nice as it could be; we need more automation to
prove Propers.

Also tune the simpl behavior of ty_own a little to be less eager with unfolding