proposition: Lemma dec_class@{} : forall q r, Decidable (class q = class r).
proof: Proof. intros q r. destruct (dec (equiv q r)) as [E|E]. - left. apply path,E. - right. intros E'. apply E. apply (classes_eq_related _ _ E'). Defined.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields