proposition: Lemma eqvars_trans : forall lva lvb lvc, eqvars lva lvb -> eqvars lvb lvc -> eqvars lva lvc.
proof: Proof. introv He1 He2. allrw (eqvars_prop). split; intro Hin; repeat (try(apply He1 in Hin); try(apply He2 in Hin); auto). Qed.
imports: list Omega