Definitions bool 1 Doc

At: decidable equal bool 1

1. a:
2. b:

Dec(a = b)

By:
Unfold `decidable` 0
THEN
AllBoolInd


Generated subgoals:

1 true = true true = true
2 false = true false = true
3 true = false true = false
4 false = false false = false