Nuprl - Pf assert iff btrue rw

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

At: assert iff btrue rw

P:. P P = true

By: Analyze 0 THEN Unfold `guard` 0

Generated subgoal:

1 1. P:
P P = true

About:

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