fact: Fixpoint arrayLookupOpt(A B : Set)(eqd : EqDec A)(ls : list (option (A * B)))(a : A) := match ls with | nil => None | o :: ls' => match o with | None => arrayLookupOpt _ ls' a | Some (a', b') => if (eqb a a') then (Some b') else (arrayLookupOpt _ ls' a) end end.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold