proposition: Lemma Acc_var : forall x, Acc (one_step R) (Var x).
proof: Proof. intro x; apply Acc_intro; intros s H; inversion H as [t1 t2 H' | f' l1 l2 H']; subst. inversion H' as [t1 t2 sigma H'' H3 H''']; subst; destruct t2 as [x2 | f2 l2]. absurd (R t1 (Var x2)); trivial; apply HR. simpl in H'''; discriminate. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)