proposition: Lemma arrayLookup_app_none : forall ls d d' v', arrayLookup ls d = None -> arrayLookup (ls ++ (d, v') :: nil) d' = arrayLookup ((d, v') :: ls) d'.
proof: Proof. induction ls; intuition; simpl in *. case_eq (eqb d a0); intuition; rewrite H0 in H. discriminate. case_eq (eqb d' d); intuition. rewrite eqb_leibniz in H1. subst. case_eq (eqb d a0); intuition. rewrite eqb_leibniz in H1. subst. rewrite eqb_refl in H0. discriminate. eapply arrayLookup_app_some_eq. trivial. specialize (IHls d d'). case_eq (eqb d' a0); intuition. rewrite H1 in IHls. eapply IHls. trivial. Qed.
imports: FCF.Crypto FCF.Fold Permutation