proposition: Lemma disjointSwapLVar: forall {G : CFGV} {vc : VarSym G} (lva lvb: list (vType vc)) sw, disjoint (lva ++ ALRange sw ++ ALDom sw) lvb -> disjoint (swapLVar sw lva) lvb.
proof: Proof. induction lva; cpx. introv Hdis. allsimpl. match goal with [ |- ?C] => remember C as concl end. repeat(disjoint_reasoning). subst concl. apply disjoint_cons_l. dands; cpx. - apply IHlva; repeat(disjoint_reasoning). - pose proof (swapVarImplies sw a ) as XX. specialize (XX _ eq_refl). repeat(in_reasoning); cpx. rw XX; cpx. Qed.
imports: Swap AssociationList Eqdep_dec