proposition: Lemma eqvars_app : forall la lb ra rb, eqvars la lb -> eqvars ra rb -> eqvars (app la ra) (app lb rb).
proof: Proof. introv Ha Hb. allrw eqvars_prop. dtiffs2. split; introv Hin; apply in_app_iff; apply in_app_iff in Hin; dorn Hin; try (left;eauto;fail) ; try (right;eauto;fail). Qed.
imports: list Omega