proposition: Lemma swapLVarDisjChain : forall {G : CFGV} {vc : VarSym G} (lv : list (vType vc)) (vsa vs vsb : list (vType vc)), length vs = length vsa -> length vs = length vsb -> no_repeats vs -> no_repeats vsb -> disjoint vs (vsa ++ vsb ++ lv) -> disjoint vsb (vsa ++ lv) -> swapLVar ((combine vsa vs) ++ (combine vs vsb)) lv = swapLVar (combine vsa vsb) lv.
proof: Proof. induction lv; cpx. intros. allsimpl. repeat (disjoint_reasoning). f_equal; cpx. - apply swapVarDisjChain; cpx; repeat(disjoint_reasoning); cpx. - apply IHlv; repeat(disjoint_reasoning); cpx. Qed.
imports: Swap AssociationList Eqdep_dec