nic-justim Show Code edit
# Show equivalence between implication and the Nicod version. To derive
# [[nic-dfim]], apply [[nic-justbi]].
thm (nic-justim () () (<-> (-> ph ps) (-/\ ph (-/\ ps ps))) ph ps ps nic-justlem ph ps anidmdbi bitr2i)
(<-> (-> ph ps) (-/\ ph (-/\ ps ps)))
edit