2. A Discrete
3. k :
4. f :
k
A
5. {a:A|
i:k. a = f(i) } 
Type
6. f
k{a:A| i:k. a = f(i) }
7. b : A
8.
i:k. b = f(i) [not for witness]
9. e : A
A
10.
x,y:A. (x e y) 
x = y
a:k. f(a) = b {a:A| i:k. a = f(i) A }
kA
i:k. a = f(i) } Type
k{a:A| i:k. a = f(i) }
i:k. b = f(i) [not for witness]
A
x,y:A. (x e y) x = y
a:k. f(a) = b {a:A| i:k. a = f(i) A }| By: |
 j.(f(j)) e b) {p:(k)| i:k. p(i) } Asserted
THEN Inst: Thm* k:, p:{p:(k)| i:k. p(i) }. (least i:. p(i)) k
Using:[k | j.(f(j)) e b]
THEN (ReduceSOAps Hyp:-1) |
| 1 |
(j.(f(j)) e b) {p:(k)| i:k. p(i) } | 3 steps |
| 2 |
j.(f(j)) e b) {p:(k)| i:k. p(i) }
12. (least i: . (f(i)) e b) k
a:k. f(a) = b {a:A| i:k. a = f(i) A } | 5 steps |
About:
 |  |  |  |  |  |
 |  |  |  |  |
 |