proposition: Lemma numberedMap_length : forall (A B : Set)(ls : list A)(f : nat -> nat -> A -> B), length (numberedMap f ls) = length ls.
proof: Proof. intuition. unfold numberedMap. rewrite map_length. repeat rewrite zip_length. apply allNatsLt_length. apply allNatsLt_length. Qed.
imports: FCF.FCF Permutation