proposition: Lemma arrayLookup_app_ne : forall ls d r d', d <> d' -> arrayLookup (ls ++ (d, r) :: nil) d' = arrayLookup ls d'.
proof: Proof. induction ls; intuition; simpl in *. case_eq (eqb d' d); intuition. rewrite eqb_leibniz in H0. subst. intuition. case_eq (eqb d' a0); intuition. Qed.
imports: FCF.Crypto FCF.Fold Permutation