proposition: Lemma length_flatten : forall {A} seq, List.length (flatten seq) = List.fold_right (compose plus (@List.length A)) 0 seq.
proof: Proof. intros. pose proof (length_flatten_aux seq 0) as H; simpl in H; eauto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Fiat.Common Coq.Arith.Arith