nic-isw1 Show Code edit
# Inference version of [[nic-swap]]. (Contributed by Jeff Hoffman,
# 17-Nov-2007.)
thm (nic-isw1 () (nic-isw1.1 (-/\ th ph)) (-/\ ph th) nic-isw1.1 th ph nic-swap nic-mp)
(-/\ ph th)
edit