proposition: Lemma DisjointEquivariantRev : forall {G : CFGV} {vc : VarSym G} la lb (sw : Swapping vc), disjoint (swapLVar sw la) (swapLVar sw lb) -> disjoint la lb.
proof: Proof. introv Hd. apply DisjointEquivariant in Hd. specialize (Hd (rev sw)). rewrite swapLVarApp in Hd. rewrite swapLVarApp in Hd. autorewrite with fast in Hd. trivial. Qed.
imports: Swap AssociationList Eqdep_dec