proposition: Lemma remove_nvars_cons_r : forall l v vars, remove_nvars l (v :: vars) = if memvar v l then remove_nvars l vars else v :: remove_nvars l vars.
proof: Proof. intros; unfold remove_nvars. rewrite diff_cons_r; auto. Qed.
imports: list Omega