proposition: Lemma Surjective_list_carac A B (f:A->B): Surjective f <-> (forall lB, exists lA, incl lB (map f lA)).
proof: Proof. split. - intros Su lB. induction lB as [|b lB IH]. + now exists nil. + destruct (Su b) as (a,E). destruct IH as (lA,IC). exists (a::lA). simpl. rewrite E. intros x [X|X]; simpl; intuition. - intros H y. destruct (H (y::nil)) as (lA,IC). assert (IN : In y (map f lA)) by (apply (IC y); now left). rewrite in_map_iff in IN. destruct IN as (x & E & _). now exists x. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec