[STATEMENT]
lemma insert_in_traverse_pairs [rewrite]:
  "tree_sorted t \<Longrightarrow> in_traverse_pairs (tree_insert x v t) = ordered_insert_pairs x v (in_traverse_pairs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tree_sorted t \<Longrightarrow> in_traverse_pairs (tree_insert x v t) = ordered_insert_pairs x v (in_traverse_pairs t)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tree_sorted t \<Longrightarrow> in_traverse_pairs (tree_insert x v t) = ordered_insert_pairs x v (in_traverse_pairs t)
[PROOF STEP]
@induct t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tree_sorted t \<Longrightarrow> in_traverse_pairs (tree_insert x v t) = ordered_insert_pairs x v (in_traverse_pairs t)
[PROOF STEP]
@qed