proposition: Theorem build_list : forall E, E_compat E -> IFinite eqA E -> forall (G:seq A -> seq A) (HG1: forall X, r_subset X (G X)) (HG2: forall X, (gpred_list E) X -> (gpred_list E) (G X)), forall X, (gpred_list E) X -> { Y | r_subset X Y /\ (gpred_list E) Y /\ r_subset (G Y) Y }.
proof: Proof. move => E hE hfE G hG1 hG2 X hX. have h: Acc (gpred_list E) sup X. by apply: wf_sup. elim: h hX=> Y hp hi hX. clear X. rename Y into X. elim: (r_subset_dec (G X) X) => hsub. - exists X; split. by apply/R_elim. by split. - case: (hi (G X)). * by apply: hG2. * apply/sub_elim. split. apply/R_elim. by apply :hG1. elim: (nR_dec (G X) X) => [| hneq]. move/nR_elim => [a h1 h2]. by exists a. elim: hsub. move => hn. elim: hneq. done. * by apply: hG2. * move => Y [h1]. move/R_elim:h1 => h1. move => [h2]. move/R_elim => h3. exists Y; split. apply/R_elim. move => x hx. apply: h1. move/R_elim : (hG1 X). by apply. split. done. by apply/R_elim. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)