proposition: Lemma ALSwitchCombine : forall {K V} (lv: list V) (lk : list K) , combine lv lk = ALSwitch (combine lk lv).
proof: Proof. induction lv; allsimpl. - destruct lk; cpx. - destruct lk; cpx. allsimpl. f_equal. cpx. Qed.
imports: list Omega