T
3. (
x,y:T. f1(x,y) 
x = y) & f1 
TT4. f2: T
T5. (
x,y:T. f2(x,y) x = y) & f2 TT
f1 = f2
}
}
f1 = f2 TT
| 1 | 2. f1: TT 3. ( x,y:T. f1(x,y) x = y) & f1 TT4. f2: T T5. ( x,y:T. f2(x,y) x = y) & f2 TT f1 = f2 |
About:
 |  |  |  |