 which can be read as “if something is true of a false proposition then if it true of a true proposition, it is true of any proposition” (C00 is a true proposition). The supreme achievements of compression using variable functors were made by Meredith, who showed (as quoted by Łukasiewicz, referring to an apparently unpublished paper) that the whole of classical propositional logic with variable functors can be based on the single axiom