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

At: int seg well founded up 1 1

1. i:
2. j: {i...}
3. WellFnd{u}({i...};x,y.x < y)

WellFnd{u}({i..j};x,y.x < y)

By: Using [`B',{i..j};`f',(x.x)] (FwdThru 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))) [3])

Generated subgoal:

14. WellFnd{u}({i..j};x,y.(x.x)(x) < (x.x)(y))
WellFnd{u}({i..j};x,y.x < y)


About:
intless_thanlambda

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