proposition: Lemma constantMapEq : forall {A B : Type} (f: A-> B), constantFn f -> forall l1 l2, length l1 = length l2 -> map f l1 = map f l2.
proof: Proof. introv Hc. repnud Hc. induction l1 as [| h1 t1 Hind]; introv Hleq; destruct l2; inverts Hleq;[|]; simpl. auto. f_equal; auto; congruence. Defined.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega Coq.Logic.Eqdep_dec