proposition: Lemma rel_map_listRepeat : forall (A B : Set)(lsa : list A)(rel : A -> B -> Prop) b, (forall a, In a lsa -> rel a b) -> rel_map rel lsa (listRepeat b (length lsa)).
proof: Proof. induction lsa; intuition; simpl in *. econstructor. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation