proposition: Theorem arrayLookup_insertInOrder_ne : forall (ls : list (A * B)) a1 a2 b, a1 <> a2 -> arrayLookup _ (insertInOrder ls a1 b) a2 = arrayLookup _ ls a2.
proof: Proof. induction ls; intuition idtac; simpl in *. case_eq (eqb a2 a1); intuition idtac. rewrite eqb_leibniz in H0. subst. intuition idtac. case_eq (leA a1 a0); intuition idtac. simpl. case_eq (eqb a2 a1); intuition idtac. rewrite eqb_leibniz in H1. subst. intuition idtac. simpl. case_eq (eqb a2 a0); intuition idtac. eauto. Qed.
imports: FCF FCF.PRF Permutation