proposition: Lemma NoRepeatsEquivariant : forall {G : CFGV} {vc : VarSym G}, @EquiVariantRelUn G vc _ (fun x s => swapLVar s x) (no_repeats).
proof: Proof. unfold EquiVariantRelUn. introv X. intros. induction ta; cpx. inverts X. allsimpl. constructor; cpx. apply NegLInEquivariant. trivial. Qed.
imports: Swap AssociationList Eqdep_dec