Be careful not to confuse variables and constants. If

Be careful about the use of free variables in formulas. The formula
`x = {} => subset(x, y)` correctly (albeit awkwardly) expresses the fact
that the empty set is a subset of any set. However, its converse,
`subset(x, y) => x = {}`, does not express the fact that any set that is a
subset of all sets must be the empty set. That fact is expressed by the
equivalent formulas `\A x (\A y subset(x, y) => x = {})` and
`\A x \E y (subset(x, y) => x = {})`.

An axiom or conjecture of the form `when A yield B` has the same logical
content as one of the form `A => B`, but different operational content.
Given the axiomization

LP will automatically derive the factdeclare variable x: Bool declare operators a: -> Bool f, g, h: Bool -> Bool .. assert when f(x) yield g(x); g(x) => h(x); f(a) ..

A multiple-hypothesis deduction rule of the form `when A, B yield C` has the
same logical content as a single-hypothesis rule of the form
`when A /\ B yield C`. They differ operationally in that, if the user
asserts or proves two formulas that are matched by `A` and `B`, LP
will apply the multiple-hypothesis rule but not the single-hypothesis rule.