Proof search now tries appropriate constructors

It will take the first one which works, which will not always be what
you want, of course, but if there is enough structure in the type then
it limits the ones which are valid.

\o in vim invokes proof search.