fact: Definition F_rec2_compute {T sT} dclass dequiv x y : @F_rec2 T sT dclass dequiv (' x) (' y) = dclass x y := 1.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields