Nuprl - Pf discrete equality unique 1 1 1 1 1 1 1 1 1

(14steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc

At: discrete equality unique 1 1 1 1 1 1 1 1 1

1. T: Type
2. f1: TT
3. f1 TT
4. f2: TT
5. f2 TT
6. v: T
7. w: T
8. b1:
9. f1(v,w) = b1
10. b2:
11. f2(v,w) = b2
12. b1 v = w
13. b2 v = w

b1 = b2

By: OnHyps [8;9] BoolInd THEN TryOnAllHyps Reduce THEN Reduce 0

Generated subgoals:

1 8. f1(v,w) = true
9. f2(v,w) = false
10. True v = w
11. True (v = w)
12. False v = w
13. False (v = w)
true = false

2 8. f1(v,w) = false
9. f2(v,w) = true
10. False v = w
11. False (v = w)
12. True v = w
13. True (v = w)
false = true

About:

(14steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc

1	8. `f1(v,w) = true` 9. `f2(v,w) = false` 10. `True v = w` 11. `True (v = w)` 12. `False v = w` 13. `False (v = w)` `true = false`
2	8. `f1(v,w) = false` 9. `f2(v,w) = true` 10. `False v = w` 11. `False (v = w)` 12. `True v = w` 13. `True (v = w)` `false = true`