[STATEMENT]
lemma lookup_insert [simp]:
  "lookup (insert (k :: 'a) v t) = (lookup t)(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (RBT_Mapping2.insert k v t) = lookup t(k \<mapsto> v)
[PROOF STEP]
by transfer (simp add: ID_ccompare_neq_None 
  linorder.rbt_lookup_rbt_insert[OF mapping_linorder])