Z_ind3@{i j} (P : Z -> Z -> Z -> Type@{i}) {sP : forall x y z : Z, IsHProp (P x y z)} (dclass : forall x y z : PairT.T N, P (' x) (' y) (' z)) : forall x y z : Z, P x y z. Proof. apply (@Z_ind (fun x => forall y z, _));intros x. 2:apply (Z_ind2@{i j} _);auto. apply (@istrunc_forall@{UN j j} _). intros. apply istrunc_forall@{UN i j}. Defined.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.