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



1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. zz : 
  n:. (n < zz)  (P(n)) 

latex

 by (%S% \p.AbSetHD (get_int_arg `hn` p) p) 

latex

 1: 

 1: 3. zz : 
 1: 4. zz  0 
 1:   n:. (n < zz)  (P(n))
 .

Definitions	, s = t, #$n, f(a), a < b, P  Q, , x:AB(x), A  B, {x:A| B(x)} , x:A. B(x), i  j , t  T,
Lemmas	nat properties