Nuprl - Pf assert_elim 1

Definitions bool 1 Doc

At: assert elim 1

1. b:
2. b

b = true

By: BoolInd 1

Generated subgoals:

1 1. true
true = true

2 1. false
false = true