proved ZZBiRecursionEquiv, with computation rule

Definition ZZBiRecursionEquiv (P:ZZ->Type) (IH :forall i, weq (P i) (P(1+i))) :
  weq (total2 (ZZBiRecursionData P IH)) (P 0).