Zapart_def@{i} := ltac:(first [exact Zapart_def'@{Uhuge i}| exact Zapart_def'@{i}]). Global Instance ishprop_Zapart : is_mere_relation _ Zapart. Proof. unfold Zapart;exact _. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.