fact: Definition F_rec_compute T sT dclass dequiv x : @F_rec T sT dclass dequiv (' x) = dclass x := 1.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields