fact: Definition F_compute_path P {sP} dclass dequiv q r (E : equiv q r) : apD (@F_rect P sP dclass dequiv) (path E) = dequiv q r E := quotient_ind_compute_path _ _ _ _ _ _ _ _.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields