proposition: Lemma insert_eq_insert_1: forall A x a1 a2 (e1 e2 : env A), insert x a1 e1 = insert x a2 e2 -> a1 = a2.
proof: Proof. intros. assert (lookup x (insert x a1 e1) = Some a1). eauto using lookup_insert_bingo. assert (lookup x (insert x a2 e2) = Some a2). eauto using lookup_insert_bingo. congruence. Qed.
imports: List Dblib(DblibTactics DeBruijn)