Nuprl - Pf beq

p,q:. p = q = true p = q

By: Unfold `beq` 0 THEN GenRepD THEN BoolCases 1 THEN BoolCases 1 THEN Try (Reduce 0) THEN Try (Reduce -1)

Generated subgoals:

None

About: