(4steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: int seg well founded up 1 1 1
1. i:
2. j: {i...}
3. WellFnd{u}({i...};x,y.x < y)
4. WellFnd{u}({i..j};x,y.(x.x)(x) < (x.x)(y))

WellFnd{u}({i..j};x,y.x < y)
By:
Reduce 4
THEN
Trivial
Generated subgoals:

None

About:
intless_thanlambdaapply

(4steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc