proposition: Theorem in_alphabet_inv : forall (c : code) (a : A) (l : list A), in_alphabet (a :: l) c -> in_alphabet l c.
proof: Proof. intros c a l H; red in |- *. intros a1 H1; apply H; simpl in |- *; auto. Qed.
imports: Coq(Sorting.Permutation)