alnfi Show Code edit
## Reproved for integers directly from the natural number versioz.
thm (alnfi ((ph x)) () (-> ph (A. x ph))
ph x z.alnfi
(-> ph (z.A. x ph))
x ph df-al bicomi
(<-> (z.A. x ph) (A. x ph))
sylib
(-> ph (A. x ph))
)
edit