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