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