proposition: Lemma tailEquivariant : forall {G : CFGV} {vc : VarSym G}, @EquiVariantFn G vc _ _ (fun x s => swapLLVar s x) (fun x s => swapLLVar s x) (@tail _).
proof: Proof. intros. unfolds_base. intros. destruct ta; cpx. Qed.
imports: Swap AssociationList Eqdep_dec