modified formalization of axiom2 in THF and Isabelle, coincides now with Scott's version