proposition: Theorem not_in_find_code : forall a l, (forall p, ~ In (a, p) l) -> find_code a l = [].
proof: Proof. intros a l; elim l; simpl in |- *; auto. intros (a1, l1) l0 H H0. case (A_eq_dec a a1); auto. intros H1; case (H0 l1); rewrite H1; auto. intros H1; apply H; intros p; red in |- *; intros Hp; case (H0 p); auto. Qed.
imports: Coq(Sorting.Permutation)