proposition: Lemma length_insert_reverse_1: forall A (e : env A) k x a, length (insert x a e) <= k -> x < k.
proof: Proof. intros. erewrite length_insert_general in * by reflexivity. mymax. Qed.
imports: List Dblib(DblibTactics DeBruijn)