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; auto. intros H; case H. intros a0 l0 H [H0|H0]; auto. exists (snd a0); left; rewrite <- H0; case a0; simpl; auto. case H; auto; intros l1 Hl1; exists l1; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat