proposition: Lemma nf_var : forall v, nf (one_step R) (Var v).
proof: Proof. intros v s H. inversion H; clear H; subst. inversion H0; clear H0; subst. destruct t2 as [v2 | f2 l2]. absurd (R t1 (Var v2)); trivial. discriminate. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)