proposition: Lemma concat_app: forall (A : Type) e1 (e2 e3 : list A), concat e1 (e2 ++ e3) = concat (concat e1 e2) e3.
proof: Proof. intros A e1 e2 e3. generalize e1. clear e1. induction e2; intro e1; simpl; auto. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)