fact: Fixpoint decode_aux (c : code) (head m : list bool) {struct m} : list A := match m with | [] => match find_val head c with | Some a => a :: [] | None => [] end | a :: m1 => match find_val head c with | Some a1 => a1 :: decode_aux c (a :: []) m1 | None => decode_aux c (head ++ a :: []) m1 end end.
imports: Coq(Sorting.Permutation)