When applied to a term of the form !p. t \/ u, where no variable in p is
free in both t and u, PFORALL_OR_CONV returns a theorem of one of three
forms, depending on occurrences of the variables from p in t and u.
If variables from p are free in t but not in u, then the theorem:
|- (!p. t \/ u) = (!p. t) \/ u
|- (!p. t \/ u) = t \/ (!t. u)
|- (!p. t \/ u) = (!p. t) \/ (!p. u)