proposition: Lemma insert_eq_insert_2: forall A x a1 a2 (e1 e2 : env A), insert x a1 e1 = insert x a2 e2 -> forall b, insert x b e1 = insert x b e2.
proof: Proof. induction x; simpl; intros. - congruence. - destruct e1; destruct e2; match goal with h: _ = _ |- _ => injection h; clear h; intros end; f_equal; try congruence; eauto. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)