Nuprl - Pf assert of eq bool iff equal bool 1

1. b1:
2. b2:

b1=b2 b1 = b2

By: BoolInd -1 THEN BoolInd -1 THEN Unfold `eq_bool` 0 THEN BoolEval THEN Rewrite (HigherC assert_evalC) 0

Generated subgoals:

1 1. false = true
False

2 1. true = false
False

About: