proposition: Theorem in_alphabet_cons : forall (m : list A) c a ca, In (a, ca) c -> in_alphabet m c -> in_alphabet (a :: m) c.
proof: Proof. intros m c a ca H H0; red in |- *; simpl in |- *. intros a1 [H1| H1]. exists ca; rewrite <- H1; auto. case (H0 a1); auto. Qed.
imports: Coq(Sorting.Permutation)