fact: Fixpoint mod_rewrites t (mds : list mod_data) : option (list term) := match mds with | nil => Some nil | md :: mds' => match mod_rewrite t md with | None => None | Some u => match mod_rewrites u mds' with | None => None | Some us => Some (u::us) end end end.
imports: Coq(Euclid Wf_nat) CoLoR(ATrs LogicUtil ALoop ListUtil RelUtil NatUtil APosition AMatching ARelation)