fact: Fixpoint find_code (a : A) (l : code) {struct l} : list bool := match l with | [] => [] | (b, c) :: l1 => match A_eq_dec a b with | left _ => c | right _ => find_code a l1 end end.
imports: Coq(Sorting.Permutation)