proposition: Theorem in_find_map : forall p a l b, In (a, l) p -> find_code a (map (fun v : A * list bool => match v with | (a1, b1) => (a1, b :: b1) end) p) = b :: find_code a p.
proof: Proof. intros p; elim p; simpl in |- *; auto. intros a l b H; case H. intros (a1, l1) l H a0 l0 b [H0| H0]; auto. case (A_eq_dec a0 a1); auto. intros HH; case HH; injection H0; auto. case (A_eq_dec a0 a1); auto. intros n; apply (H a0 l0 b); auto. Qed.
imports: Coq(Sorting.Permutation)