proposition: Lemma length_map : forall A B (l:list A) (f:A->B), length (map f l) = length l.
proof: Proof. Proof using. intros. unfold length. rewrite~ length_map. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)