proposition: Lemma map_eq_cons : forall l l' b, map l = b :: l' -> exists a tl, l = a :: tl /\ f a = b /\ map tl = l'.
proof: Proof. intros l l' b Heq. destruct l as [|a l]; inversion_clear Heq. exists a, l; repeat split. Qed.
imports: PeanoNat