proposition: Lemma NegLInEquivariant : forall {G : CFGV} {vc : VarSym G}, @EquiVariantRel G vc _ _ (fun x s => swapVar s x) (fun x s => swapLVar s x) (fun x l => !LIn x l).
proof: Proof. unfold EquiVariantRel. intros. induction tb; cpx. allsimpl. introv Hc. apply H. dorn Hc;[left; subst | right]; cpx. - apply swapVarInj in Hc; trivial. - apply IHtb in Hc; cpx. Qed.
imports: Swap AssociationList Eqdep_dec