proposition: Lemma rel_map_left_total_strong' : forall (A B : Type)(lsa : list A)(P : A -> Prop)(rel : A -> B -> Prop), (forall a, P a -> exists b, rel a b) -> (forall a, In a lsa -> P a) -> exists lsb, rel_map rel lsa lsb.
proof: Proof. induction lsa; intuition. exists nil. econstructor. edestruct (IHlsa _ _ H). intuition. destruct (H a). eapply H0. simpl. intuition. exists (x0 :: x). econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation