proposition: Lemma Acc_lt_var : forall x, Acc lt (Var x).
proof: Proof. intro x; constructor; intros t lt_t_var_x. elim (var_are_min lt_t_var_x). Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)