proposition: Lemma length_concat_replicate: forall A (a : A) (e1 : env A) n1 n2 n, length e1 <= n1 -> n1 + n2 = n -> length (concat e1 (replicate n2 a)) <= n.
proof: Proof. intros. eapply length_concat. eauto. rewrite length_replicate. eauto. Qed.
imports: List Dblib(DblibTactics DeBruijn)