fact: Fixpoint find_val (a : list bool) (l : code) {struct l} : option A := match l with | [] => None | (b, c) :: l1 => match list_eq_dec Bool.bool_dec a c with | left _ => Some b | right _ => find_val a l1 end end.
imports: Coq(Sorting.Permutation)