(3steps total) PrintForm Definitions ElisTarskiPf A Sections NuprlLIB Doc

At: qnot subx 1
1. t: Term
2. e: Term
SUBX(NOT(t); e) = NOT(SUBX(t; e))
By: Unfold `subx` 0
Generated subgoal:

1 NOT(t)[e/X] = NOT(t[e/X])1 step

About:
equal

(3steps total) PrintForm Definitions ElisTarskiPf A Sections NuprlLIB Doc