proposition: Lemma LInEquivariant : forall {G : CFGV} {vc : VarSym G}, @EquiVariantRel G vc _ _ (fun x s => swapVar s x) (fun x s => swapLVar s x) (LIn).
proof: Proof. unfold EquiVariantRel. intros. induction tb; cpx. allsimpl. dorn X;[left; subst | right]; cpx. Qed.
imports: Swap AssociationList Eqdep_dec