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