proposition: Lemma rangeFreeVarsEquivariant : EquiVariantFn (@swapSub _ vc) (fun x s => swapLVar s x) (@rangeFreeVars _ _ ).
proof: Proof. unfold EquiVariantFn. intros sub sw. induction sub as [| (v,t) sub Hind]; cpx. allsimpl. rw rangeFreeVars_cons. rw rangeFreeVars_cons. rewrite swapLVar_app. f_equal;cpx. rewrite (tcase freevarsEquivariant). refl. Qed.
imports: Term AssociationList Swap AlphaEqProps SubstAux