proposition: Lemma prune x l l' : Permutation (x :: l) l' -> find x l'.
proof: Proof. intros P. assert (i : In x l'). apply Permutation_in with (x :: l). auto. left; auto. clear -i. induction l'. inversion i. simpl. simpl in i. destruct (pe x a). auto. apply IHl'. destruct i; auto. congruence. Qed.
imports: Arith List Permutation