proposition: Theorem map_eq_length_eq : forall A B (f g : A -> B) la1 la2, map f la1 = map g la2 -> length la1 = length la2.
proof: Proof. introv Hmap. apply (apply_eq (@length B)) in Hmap. repeat (rewrite map_length in Hmap); trivial. Qed.
imports: UsefulTypes bin_rels Omega