Inference at * 1 1 2 1 1 2 1 1 1 
Iof proof for Lemma complete nat ind with y:



1. P : {k}
2. g : i:. (j:i. P(j))  P(i)
3. Y(f,x. g(x,f))  VoidVoid
4. n : 
5. 0 < n
6. Y(f,x. g(x,f))  (m:(n - 1). P(m))
7. r : n
8. r = (n - 1)
  g(r,Y(f,x. g(x,f)))  P(r) 

latex

 by MemberEqCD 

latex

 1: .....subterm..... T:t1:n

 1:   g(r)  (j:r. P(j))P(r)
 2: .....subterm..... T:t2:n

 2:   Y(f,x. g(x,f))  (j:r. P(j))
 .

Definitions

t  T