nic-swap Show Code edit
# {{{-/\}}} is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.)
thm (nic-swap () () (-/\ (-/\ th ph) (-/\ (-/\ ph th) (-/\ ph th))) ph nic-id ph ph ph ta th nic-ax nic-mp)
(-/\ (-/\ th ph) (-/\ (-/\ ph th) (-/\ ph th)))
edit