;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)))
;x,y.x < y)| Rank | Theorem | Name |
| 3 |
Thm* WellFnd{i}(;x,y.|x| < |y|) | [int_mag_well_founded] |
| cites | ||
| 1 |
Thm* r:(AAProp), B:Type, f:(BA).
WellFnd{i}(A;x,y.r(x,y)) WellFnd{i}(B;x,y.r(f(x),f(y))) | [inv_image_ind] |
| 2 |
Thm* WellFnd{i}(;x,y.x < y) | [nat_well_founded] |