Z_ind@{i} (P : Z -> Type@{i}) {sP : forall x : Z, IsHProp (P x)} (dclass : forall x : PairT.T N, P (cast (PairT.T N) Z x)) : forall x : Z, P x. Proof. apply (Z_rect@{i} P dclass). intros;apply path_ishprop@{i}. Defined.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.