;x,y.|x|<|y|)
;x,y.x<y)
r:(T
TProp), S:Type, f:(ST).
Thm* WellFnd{i}(T;x,y.r(x,y))
WellFnd{i}(S;x,y.r(f(x),f(y)))| Rank | Theorem | Name |
| 3 | ;x,y.|x|<|y|) | [int_mag_well_founded] |
| cites the following: | ||
| 2 | ;x,y.x<y) | [nat_well_founded] |
| 0 | r:(TTProp), S:Type, f:(ST).
Thm* WellFnd{i}(T;x,y.r(x,y)) WellFnd{i}(S;x,y.r(f(x),f(y))) | [inv_image_ind_a] |