Nuprl - Pf assert of eq bool iff equal bool 1 1

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

At: assert of eq bool iff equal bool 1 1

1. false = true

False

By: ApFunToHypEquands `z' if z 0 else 1 fi -1 THEN AbReduce -1

Generated subgoal:

1 2. 1 = 0
False

About:

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