};x,y.(
x.j-x)(x) < (x.j-x)(y))
WellFnd{u}({i..j};x,y.x > y)
WellFnd{u}({i..j};x,y.x > y)};`f',(x.j-x)]
(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)))
[3])| 1 | 4. WellFnd{u}({i..j};x,y.(x.j-x)(x) < (x.j-x)(y)) WellFnd{u}({i..j};x,y.x > y) |
About:
 |  |  |  |  |