 The proof has recently been analysed to an unprecedented degree of detail and precision by Benzmüller &amp; Paleo 2014 with the help of automated theorem provers. A major challenge faced by these authors was the lack of a HOML-based theorem prover that could carry out the work but this was circumvented by embedding the logic into the classical higher-order logic (HOL) already offered by existing theorem provers like LEO-II, Satallax and the countermodel finder Nitpick. Details of the syntactic and semantic embedding are given in their paper and it consists of encoding HOML formulas as HOL predicates via mappings, expansions, and βη-conversions. The mapping associates HOML types α, terms sα, and logical operators θ with corresponding HOL “raised” types ⌈α⌉, type-raised terms ⌈sα⌉, and type-raised logical operators θ•. If μ and ο are, respectively, the types of individuals and Booleans then ⌈μ⌉ = μ and ⌈ο⌉ = σ where σ is shorthand for ι → ο with ι as the type of possible worlds; as for function types, ⌈β→γ⌉ = ⌈β⌉→⌈γ⌉. For type-raised terms, ⌈sα⌉ is defined inductively on the structure of sα as the following example illustrates: