proposition: Lemma concat_app : forall m1 m2 : list (list A), concat (m1 ++ m2) = concat m1 ++ concat m2.
proof: Proof. Proof using. intros m1. induction m1; intros. { rewrite concat_nil. rew_list~. } { rew_list. do 2 rewrite concat_cons. rew_list. fequals. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)