Please read the file KeyFormulasSpec.tex and 'Ono_PofN.tex'. Formalize and prove Key Formula~\ref{Formula1} and Key Formula~\ref{Formula2}. The proofs must be fully sorry-free. Do not add axioms or leave stray sorrys.