 The proof in Benzmüller &amp; Paleo 2014 is presented here, including the axioms and definitions as well as the derivation of its four main results—T1, C, T2, T3—all written in the type-decorated type-raised higher-order logic notation resulting from the embedding. The proof steps are not fully expanded—note the presence of type-raised connectives—and the inferential moves are not broken down to lower levels of detail. Borrowing a phrase from Bertrand Russell (Urquhart 1994), this was done to spare the reader of the “kind of nausea” that the fully detailed automated proof would cause: 