proposition: Lemma iter_step_commut : forall k (p : problem), iter_step k (step p) = step (iter_step k p).
proof: Proof. induction k. refl. simpl. intro. rewrite IHk. refl. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)