proposition: Lemma Context_Acc_var : forall R, (forall x t, ~ (R t (Var x))) -> forall x, Acc (C_step R) (Var x).
proof: Proof. intros R HR x; apply Acc_intro. intros y H; inversion H; clear H; subst. inversion H0; clear H0; subst. destruct t2 as [x2 | f2 l2]. apply False_rect; apply (HR _ _ H2). discriminate. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)