Nuprl - Pf not_assert_elim 1

Definitions bool 1 Doc

At: not assert elim 1

1. b:
2. b

b = false

By: BoolInd 1

Generated subgoals:

1 1. true
true = false

2 1. false
false = false