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

.....basecase..... NILNIL

1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
  n:. (n < 0)  (P(n)) 

latex

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

latex

C1: 

C1: 3. n : 
C1: 4. n < 0
C1:   P(n)
C2: .....wf..... NILNIL

C2: 3. n : 
C2:   (n < 0)  
C3: .....wf..... NILNIL

C3:     Type
C.

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