homotopy nat...
uniqueness lemma for nat

Lemma uniqueness (P:nat->Type) (p0:P 0) (IH:forall n, P n->P(S n)) :
    iscontr (total2 (fun f:forall n, P n =>
                       dirprod (f 0==p0) (forall n, f(S n)==IH n (f n)))).