proposition: Lemma list_for_n_concat : forall (A : Set) (P : A -> Prop) n1 n2 L1 L2, list_for_n P n1 L1 -> list_for_n P n2 L2 -> list_for_n P (n1+n2) (L1 ++ L2).
proof: Proof. Proof using. unfold list_for_n. introv [? ?] [? ?]. split. rew_list~. apply* Forall_app. Qed.
imports: TLC(LibList)