True ↔ ∃ k, Erdos10.sumPrimeAndTwoPows k = Set.univ \ {0, 1}