proposition: Lemma iter_step_correct : forall s p k, is_sol s p <-> is_sol s (iter_step k p).
proof: Proof. induction k; simpl. intuition. rewrite <- step_correct. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)