proposition: Lemma length_concat: forall A (e2 : list A) (e1 : env A) n1 n, length e1 <= n1 -> n1 + length e2 = n -> length (concat e1 e2) <= n.
proof: Proof. induction e2; simpl; intros. - replace n with n1 by lia. assumption. - eauto using length_insert, lia_hint_1 with lia. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)