Dec((
s.
t:T. f(t) = s)(t))s.t:T. f(t) = s)(t) }) Fin({s:S| t:T. f(t) = s })
S
s:S. Dec(t:T. f(t) = s) Fin({s:S| t:T. f(t) = s })B:(TProp). Fin(T) & (t:T. Dec(B(t))) 
Fin({t:T| B(t) })
[S;s.t:T. f(t) = s]| 1 | 7. t: S Dec((s.t:T. f(t) = s)(t)) |
| 2 | 7. Fin({t:S| (s.t:T. f(t) = s)(t) }) Fin({s:S| t:T. f(t) = s }) |
About:
 |  |  |  |  |  |  |  |