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.

Finish porting HOL Light's fol_prop.ml

Port HOL Light proof of compactness for prop. logic

Most of material from fol_prop.ml, with stuff supporting Uniformity
Lemma still to come.