"auto" now does proof search

Instead of just the "trivial" tactic, it now searches through possible
constructors.