Extend definitions in Iso.v

This is based on the paper "Reason Isomorphically!".