fact: Fixpoint arrayLookup_f (A B C : Set)(eqd : EqDec B)(ls : list ((A * B) * C))(a : B) := match ls with | nil => None | ((x, z), y) :: ls' => if (eqb a z) then (Some y) else (arrayLookup_f _ ls' a) end.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv