2. S: Type
3. f: T
S4. Fin(S) & (
s:S. Dec(
t:T. f(t) = s))
Fin(x,y:T//(f(x) = f(y))) T,S:Type, f:(TS). Fin(S) & (s:S. Dec(t:T. f(t) = s)) 
Fin(x,y:T//(f(x) = f(y)))| 1 | 1. T: Type 2. S: Type 3. f: T S4. Fin(S) & ( s:S. Dec(t:T. f(t) = s)) Fin(x,y:T//(f(x) = f(y))) |
About:
 |  |  |  |  |
 |  |  |  |