proposition: Lemma var_list_list_app : forall l1 l2, var_list_list (l1 ++ l2) = (var_list_list l1) ++ var_list_list l2.
proof: Proof. fix var_list_list_app 1; intros l1 l2; case l1; clear l1. reflexivity. intros t1 l1; simpl; rewrite <- ass_app; rewrite var_list_list_app; reflexivity. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)