z.n-z)(x) < (z.n-z)(y))
WellFnd{i}({...n};x,y.x > y)
;x,y.x < y) WellFnd{i}({...n};x,y.x > y)z.n-z)]
(FwdThru
Thm* 
r:(A
AProp), B:Type, f:(BA).
WellFnd{i}(A;x,y.r(x,y)) 
WellFnd{i}(B;x,y.r(f(x),f(y)))
[2])| 1 | 3. WellFnd{i}({...n};x,y.(z.n-z)(x) < (z.n-z)(y)) WellFnd{i}({...n};x,y.x > y) |
About:
 |  |  |  |