proposition: Fact quotient_is_enum X R Y : nat_enum_cls R -> @quotient X R Y -> nat_enum_cls (@eq Y).
proof: Proof. intros (f & Hf) (c & r & H1 & H2). exists (fun n => match f n with Some x => Some (c x) | None => None end). intros y. destruct (Hf (r y)) as (z & n & H3 & H4). exists (c z), n; rewrite H3; split; auto. rewrite <- (H1 y); apply H2; auto. Qed.
imports: List Arith Lia Permutation Relations Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat)