Nuprl - Pf not assert iff bfalse 2

(6steps) PrintForm Definitions bool 2 jlc Sections Support(jlc) Doc

At: not assert iff bfalse 2

1. P:
2. P = false

P

By: Unfold `not` 0 THEN Analyze 0

Generated subgoal:

1 3. P
False

About:

(6steps) PrintForm Definitions bool 2 jlc Sections Support(jlc) Doc