fact: Fixpoint iter_step k (p : problem) := match k with | 0 => p | S k' => step (iter_step k' p) end.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)