proposition: Lemma rel_map_length : forall (A B : Type)(lsa : list A)(P : A -> B -> Prop)(lsb : list B), rel_map P lsa lsb -> length lsa = length lsb.
proof: Proof. induction 1; intuition; simpl in *. f_equal. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation