proposition: Lemma unsuccessfull_preserved : forall k p, iter_step k p = None -> forall l, l > k -> iter_step l p = None.
proof: Proof. cut (forall k p, iter_step k p = None -> forall l, iter_step (l+k) p = None); intros. destruct (gt_plus H1). subst. apply H. hyp. elim l; clear l; simpl. hyp. intros. rewrite H0. refl. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)