proposition: Lemma empty_eq_insert: forall A x o (e : env A), empty _ = insert x o e -> False.
proof: Proof. unfold empty; intros; destruct x. - rewrite raw_insert_zero in *. congruence. - rewrite raw_insert_successor in *. congruence. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)