proposition: Lemma var_list_unfold : forall t, var_list t = match t with | Var x => (x :: nil) | Term _ l => var_list_list l end.
proof: Proof. intro t; case t; clear t; intros; reflexivity. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)