proposition: Lemma agree_insert: forall A (e1 e2 : env A) k, agree e1 e2 k -> forall x o, x <= k -> agree (raw_insert x o e1) (raw_insert x o e2) (1 + k).
proof: Proof. unfold agree. intros * H * ? n **. destruct (lt_eq_lt_dec x n) as [[] | ]; intros; do 2 lookup_insert; (apply H; lia) || reflexivity. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)