proposition: Theorem DEC_PER_list_proj_finite_discrete : { D & { _ : dec (@eq D) & { _ : finite_t D & { f : X -> D | forall x y, In x l -> In y l -> R x y <-> f x = f y } } } }.
proof: Proof. Proof using Rper Rdec Hl. destruct decidable_PER_fp_quotient with (R := T) (l := l) as [ n cls repr G1 G2 G3 ]; auto. exists (option (pos n)). exists. { red; decide equality; apply pos_eq_dec. } exists. { apply finite_t_option, finite_t_pos. } exists cls. intros x y Hx Hy; split. + intros H; apply G3; split; auto; exists y; auto. + intros H. apply G3; split; auto. red; rewrite <- G2. intros C; apply C. assert (R x x) as H1 by now apply Hl. split; eauto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(utils_list utils_decidable fin_base) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.Shared.Libs.DLW.Wf(measure_ind)