ZZTorsorRecursionEquiv with computation rule

Definition ZZTorsorRecursionEquiv {T:Torsor ZZ} (P:T->Type)
      (IH:forall t, weq (P t) (P (one + t))) :
  forall t0,
  weq (total2 (fun
          f:forall t, P t =>
            forall t, f (one + t) == IH t (f t)))
      (P t0).