r:(A
AProp), B:Type, f:(BA).
Thm* WellFnd{i}(A;x,y.r(x,y))
WellFnd{i}(B;x,y.r(f(x),f(y)))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)))| Theorem | Name |
| r:(AAProp), B:Type, f:(BA).
Thm* WellFnd{i}(A;x,y.r(x,y)) WellFnd{i}(B;x,y.r(f(x),f(y))) | [inv_image_ind] |
| cites the following: | |
| 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_tp] |