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

.....assertion..... NILNIL

1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. zz : 
4. 0 < zz
5. n:. (n < (zz - 1))  (P(n))
6. n : 
7. n < zz
  n1:. (n1 < n)  (P(n1)) 

latex

 by ((D 0) 
CollapseTHENM (D 0)) 

latex

C1: 

C1: 8. n1 : 
C1: 9. n1 < n
C1:   P(n1)
C2: .....wf..... NILNIL

C2: 8. n1 : 
C2:   (n1 < n)  
C3: .....wf..... NILNIL

C3:     Type
C.

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