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

At: qnot subx 1
1. t: Term
2. e: Term
NOT(t)/e = NOT(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 B Sections NuprlLIB Doc