support infinite quantifiers

[c-cube]

support quantifiers on datatypes, using undefined:

• ∀x. p x should become, for bound 3: p 0 ∧ p (s 0) ∧ p (s (s 0)) ∧ p (s (s (s undefined)))
• be careful about unsat/unknown
• allow such quantifiers in input
• do the same for functions? not obvious!