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