Use new drule to improve folCanonScript in compactness example

Make some PREIMAGE theorems automatic rewrites

Also remove |- SING s ==> FINITE s from the set of automatic rewrites.

The presence of this is bad because a "Once" simplification theorem
meant for s may fire when the simplifier attempts to discharge the
hypothesis, and so it won't get to fire when actually rewriting s in
the "main" goal. (And no-one uses SING.)

Knock-on effects simplify folCanonScript.sml, the experience of
writing which prompted these changes in the first place.

Complete port of HOL Light FOL compactness material

Also add a finite entailment property:

INFINITE 𝕌(:α) ⇒
(entails (:α) Γ ϕ ⇔ ∃Γ₀. FINITE Γ₀ ∧ Γ₀ ⊆ Γ ∧ entails (:α) Γ₀ ϕ)

You only need a finite number of hypotheses to get to a conclusion.
This is obvious if you have a proof system, but is true thanks to
compactness if you are just working with models.