F_ind3@{i j} (P : F -> F -> F -> Type@{i}) {sP : forall x y z, IsHProp (P x y z)} (dclass : forall x y z : Frac R, P (' x) (' y) (' z)) : forall x y z, P x y z. Proof. apply (@F_ind (fun x => forall y z, _)). - intros;apply istrunc_forall@{UR j j}. - intros x. apply (F_ind2@{i j} _). auto. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.