ax-4 Show Code edit
# roughly Margaris A5, but without the subst
## Axiom 4: Specialization
## right('Remove', '∀')
thm (ax-4 () () (-> (A. x ph) ph)
x ph z.ax-4
(-> (z.A. x ph) ph)
x ph df-al bicomi
(<-> (z.A. x ph) (A. x ph))
sylbi2
(-> (A. x ph) ph)
)
edit