proposition: Lemma arrayLookup_app_some : forall ls d d' v v', arrayLookup ls d = Some v -> arrayLookup (ls ++ (d, v') :: nil) d' = arrayLookup ls d'.
proof: Proof. induction ls; intuition; simpl in *. discriminate. case_eq (eqb d a0); intuition. rewrite H0 in H. inversion H; clear H; subst. rewrite eqb_leibniz in H0. subst. case_eq (eqb d' a0); intuition. eapply arrayLookup_app_ne. intuition. subst. rewrite eqb_refl in H. discriminate. rewrite H0 in H. case_eq (eqb d' a0); intuition. eapply IHls; eauto. Qed.
imports: FCF.Crypto FCF.Fold Permutation