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