the_es:ES. WellFnd{i}(E;x,y.(x <loc y))R:(T
TType). SWellFounded(R(x,y)) 
WellFnd{i}(T;x,y.R(x,y))| Theorem | Name |
| the_es:ES. WellFnd{i}(E;x,y.(x <loc y)) | [es-locl-wellfnd] |
| cites the following: | |
| R:(TTType). SWellFounded(R(x,y)) WellFnd{i}(T;x,y.R(x,y)) | [strongwf-implies] |