Inference at * 1 1 1 1 1 1 0 
Iof proof for Lemma comp nat ind tp:



1. P : {k}
2. i:. (j:. (j < i)  P(j))  P(i)
3. zz : 
  i:. (i < zz)  P(i) 

latex

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

latex

 1: 

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

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