proposition: Theorem insertInOrder_NoDup : forall (s : list (A * B)) a b, NoDup (fst (split s)) -> arrayLookup _ s a = None -> NoDup (fst (split (insertInOrder s a b))).
proof: Proof. induction s; intuition idtac; simpl in *. econstructor. intuition idtac. econstructor. case_eq (eqb a a0); intros. rewrite H1 in H0. discriminate. rewrite H1 in H0. remember (split s) as z. destruct z. simpl in *. case_eq (leA a a0); intros. simpl. remember (split s) as z. destruct z. simpl. inversion H; clear H; subst. econstructor. simpl; intuition idtac. subst. rewrite eqb_refl in *. discriminate. eapply arrayLookup_None_not_In in H0. intuition idtac. rewrite <- Heqz0. intuition idtac. econstructor; intuition idtac. pairInv. intuition idtac. pairInv. intuition idtac. simpl. remember (split (insertInOrder s a b0)) as z. destruct z. simpl. inversion H; clear H; subst. econstructor. assert (arrayLookup _ (insertInOrder s a b0) a0 = None). rewrite arrayLookup_insertInOrder_ne. eapply notInArrayLookupNone. rewrite <- Heqz. intuition idtac. intuition idtac; subst. rewrite eqb_refl in *. discriminate. intuition idtac. eapply arrayLookup_None_not_In in H. intuition idtac. rewrite <- Heqz0. trivial. specialize (IHs a b0). intuition idtac. rewrite <- Heqz0 in H3. trivial. Qed.
imports: FCF FCF.PRF Permutation