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