Inference at * 1 3 1 0 1 1 1 0 1 1 
Iof proof for Lemma fincr wf2:

.....downcase..... NILNIL

1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. zz : 
4. zz < 0
5. ((zz+1)  0 )  (n:. (n < (zz+1))  (P(n)))
  (zz  0 )  (n:. (n < zz)  (P(n))) 

latex

 by D 0 

latex

 1: 

 1: 6. zz  0 
 1:   n:. (n < zz)  (P(n))
 2: .....wf..... NILNIL

 2:   (zz  0 )  
 .

Definitions	Type, s = t, n+m, #$n, , f(a), a < b, , x:AB(x), i  j , x:A. B(x), P  Q, t  T,
Lemmas	nat wf, ge wf