proposition: Theorem decidable_EQUIV_fin_quotient l R : (forall x, R x x) -> (forall x y, R x y -> R y x) -> (forall x y z, R x y -> R y z -> R x z) -> (forall x y, { R x y } + { ~ R x y }) -> (forall x : X, exists y, In y l /\ R x y) -> fin_quotient R.
proof: Proof. intros H1 H2 H3 H4 H5. destruct (@decidable_PER_fp_quotient l R) as [ n cl rp Q1 Q2 Q3 ]; simpl; auto. + intros x; split; auto; intros _; exists x; auto. + split; auto. + assert (forall x, { y | cl x = Some y }) as H. { intros x; case_eq (cl x). * intros p; exists p; auto. * intros C; exfalso. apply Q2 in C. apply C; auto. } set (cl' x := proj1_sig (H x)). assert (H' : forall x, cl x = Some (cl' x)). { intros x; apply (proj2_sig (H x)). } generalize cl' H'; clear H cl' H'; intros cl' H. exists n cl' rp. * intro x. generalize (Q1 x); rewrite H. injection 1; auto. * intros x y; rewrite Q3. split. - intros (C1 & _). apply Some_inj; rewrite <- H, <- H; auto. - intros E; rewrite H, H, E; split; auto; discriminate. 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)