proposition: Lemma shifting_context : forall R f shift l', Acc (c_in_context R shift f) l' -> Acc (c_in_context R (S shift) f) (match l' with nil => nil | _ :: l => l end).
proof: Proof. intros R f shift l Acc_l; induction Acc_l as [l Acc_l IH]. destruct l as [ | t l]. apply Acc_intro; intros y [n [H _]]; inversion H. apply Acc_intro; intros k H. apply (IH (t :: k)). unfold c_in_context in *. destruct H as [n [H1 H2]]. exists (S n); split. apply C_tail_step; assumption. rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)