proposition: Lemma length_concat_eq_sum : forall A (l:list (list A)), length (concat l) = sum (map (length (A:=A)) l).
proof: Proof. Proof using. intros. induction l; rew_listx; math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)