proposition: Lemma eqvars_remove_nvars : forall la lb ra rb, eqvars la lb -> eqvars ra rb -> eqvars (remove_nvars la ra) (remove_nvars lb rb).
proof: Proof. introv Ha Hb. allrw eqvars_prop. dtiffs2. split; introv Hin; apply in_remove_nvars in Hin; repnd; apply in_remove_nvars; split; cpx; eauto. Qed.
imports: list Omega