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