proposition: Lemma eqvars_cons_l_iff : forall v vs1 vs2, eqvars (v :: vs1) vs2 <=> (LIn v vs2 # eqvars (remove_nvar vs1 v) (remove_nvar vs2 v)).
proof: Proof. sp; repeat (rw eqvars_prop). split; intro i; sp; allrw in_remove_nvar; allsimpl. rw <- i; sp. split; sp. rw <- i; sp. apply_in_hyp p; sp; subst; sp. split; sp; subst; sp. destruct (eq_var_dec v x); subst; sp. gen_some x; allrw in_remove_nvar. discover; sp. destruct (eq_var_dec v x); subst; sp. gen_some x; allrw in_remove_nvar. discover; sp. Qed.
imports: list Omega