Add working example of LFSC proof with quantifiers.  Update quantifiers signature to avoid dependent types in side condition.