proposition: Lemma length_insert: forall A x k km1 o (e : env A), length e <= km1 -> km1 <= k - 1 -> x < k -> length (raw_insert x o e) <= k.
proof: Proof. intros. erewrite length_insert_general by reflexivity. mymax. Qed.
imports: List Dblib(DblibTactics DeBruijn)