WellFnd{i}(
;x,y.x < y)
;x,y.(
x.|x|)(x) < (x.|x|)(y)) WellFnd{i}(;x,y.|x| < |y|) WellFnd{i}(;x,y.|x| < |y|)
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)))
[lexpr{i};;
x,y. x < y;;x.|x|]| 1 | WellFnd{i}(;x,y.x < y) |
| 2 | 1. WellFnd{i}(;x,y.(x.|x|)(x) < (x.|x|)(y)) WellFnd{i}(;x,y.|x| < |y|) |
About:
 |  |  |