proposition: Lemma DisjointEquivariant : forall {G : CFGV} {vc : VarSym G}, @EquiVariantRelSame G vc _ (fun x s => swapLVar s x) (disjoint).
proof: Proof. unfold EquiVariantRelSame, EquiVariantRel. intros. induction ta; cpx. allsimpl. introv Hin Hinc. allsimpl. dorn Hin. - revert Hinc. subst. apply NegLInEquivariant. introv Hc. repeat (disjoint_reasoning). - repeat (disjoint_reasoning). disjoint_lin_contra. Qed.
imports: Swap AssociationList Eqdep_dec