2.
x,y:T. Dec(x = y)3. s: (T+T) List
4. i: T
y:T+T. Dec(inl(i) = y)
T:Type. (x,y:T. Dec(x = y)) 
(s:(T+T) List, i:T. Dec((inl(i) 
s)))
x:T, l:T List. (y:T. Dec(x = y)) Dec((x l))
| 1 | 1. T: Type 2. x,y:T. Dec(x = y)3. s: (T+T) List 4. i: T y:T+T. Dec(inl(i) = y) | 4 steps |
About:
 |  |  |  |  |  |  |  |