Nuprl - Proof: decidable equal bool 1

(8steps total) PrintForm Definitions Lemmas bool 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
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
1 step

2   false = true  false = true
3 steps

3   true = false  true = false
1 step

4   false = false  false = false
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(8steps total) PrintForm Definitions Lemmas bool 1 Sections StandardLIB Doc

1	true = true true = true	1 step
2	false = true false = true	3 steps
3	true = false true = false	1 step
4	false = false false = false	1 step