proposition: Theorem enum_quotient X R : nat_enum_cls R -> equiv X R -> dec R -> { Y : Type & { _ : dec (@eq Y) & quotient R Y } }.
proof: Proof. intros (f & Hf) H1 H2. apply enum_quotient_rec with (1 := Hf) (R := R); auto. Qed.
imports: List Arith Lia Permutation Relations Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat)