[STATEMENT]
lemma inorder_mkNode[simp]:
  "inorder (mkNode c l a r) = inorder l @ a # inorder r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Tree2.inorder (mkNode c l a r) = Tree2.inorder l @ a # Tree2.inorder r
[PROOF STEP]
by (auto simp: mkNode_def)