proposition: Theorem arrayLookup_sortDom_eq : forall (ls : list (A * B)) a, arrayLookup _ ls a = arrayLookup _ (sortDom ls) a.
proof: Proof. induction ls; intuition idtac; simpl in *. case_eq (eqb a a0); intros. rewrite eqb_leibniz in H. subst. rewrite arrayLookup_insertInOrder_same. trivial. rewrite arrayLookup_insertInOrder_ne. eauto. intuition idtac; subst. rewrite eqb_refl in *. discriminate. Qed.
imports: FCF FCF.PRF Permutation