proposition: Lemma sort_eqvars : forall vars, eqvars vars (sort vars).
proof: Proof. induction vars; simpl; sp. destruct a. trw eqvars_cons_l_iff; sp. apply insert_in. rewrite remove_nvar_insert. apply eqvars_remove_nvar; sp. Qed.
imports: list Omega