z.z-n)(x) < (z.z-n)(y))
WellFnd{i}({n...};x,y.x < y)
;x,y.x < y) WellFnd{i}({n...};x,y.x < y)z.z-n)]
(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.z-n)(x) < (z.z-n)(y)) WellFnd{i}({n...};x,y.x < y) |
About:
 |  |  |  |