fact: Fixpoint guard n (wfR: well_founded): well_founded := match n with | 0 => wfR | S n => fun x => Acc_intro (fun y _ _ => guard n (guard n wfR) y) end.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)