proposition: Theorem in_map_fst_inv : forall a (l : list (B * C)), In a (map (fst (B:=_)) l) -> exists c, In (a, c) l.
proof: Proof. intros a l; elim l; simpl in |- *; auto. intros H; case H. intros a0 l0 H [H0| H0]; auto. exists (snd a0); left; rewrite <- H0; case a0; simpl in |- *; auto. case H; auto; intros l1 Hl1; exists l1; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)