Nuprl - Pf assert iff btrue rw 1

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

At: assert iff btrue rw 1

1. P:

P P = true

By: Inst Thm* P:. P P = true [P]

Generated subgoals:

None

About:

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