Aesop rule set for finsets

This file defines finsetNonempty, an aesop rule set to prove that a given finset is nonempty.