F_ind@{i} (P : F -> Type@{i}) {sP : forall x, IsHProp (P x)} (dclass : forall x : Frac R, P (' x)) : forall x, P x. Proof. apply (@F_rect P (fun _ => istrunc_hprop) dclass). intros;apply path_ishprop. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.