I have a subgoal of the form 1. "~ (finite (UNIV :: int set))"However, I can't find a corresponding theorem using find_theorems in Isabelle/HOL. Nor was find_theorems produce successful on the terms "card (UNIV :: int set)" or "setsum ?f (UNIV :: int set)".
What is the best way to prove this subgoal? Thanks, -john