proposition: Lemma shifting_head : forall R f shift l, Acc (c_in_context R shift f) l -> mem eq shift (mu f) -> (forall t, (exists k, l = t::k) -> Acc (C_step R) t).
proof: Proof. intros R f shift l Acc_l; induction Acc_l as [l Acc_l IH]. destruct l as [ | t l]. intros _ t [l H]; discriminate. intros shift_in_mu_f. intros s [l' H]. injection H; clear H; intros; subst s l'. apply Acc_intro; intros s H. apply (IH (s :: l)). exists 0; split. left; trivial. rewrite Nat.add_comm; simpl. apply mem_impl_in with (@eq _); trivial. assumption. exists l; apply eq_refl. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)