When applied to a paired structure of variables p and a theorem A |- t,
the inference rule PGEN returns the theorem A |- !p. t, provided that
no variable in p occurs free in the assumptions A.
There is no compulsion that the variables of p should be free in t.
A |- t
------------ PGEN "p" [where p does not occur free in A]
A |- !p. t