proposition: Theorem IFinite_supwf : forall E, E_compat E -> (IFinite eqA E <-> well_founded sup (gpred_list E)).
proof: Proof. move => E hE; split => h. - by apply wf_sup. by apply sup_wf. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)