[STATEMENT]
lemma to_ordered_collection_det:
  "to_ordered_collection \<tau> \<sigma>\<^sub>1 \<Longrightarrow>
   to_ordered_collection \<tau> \<sigma>\<^sub>2 \<Longrightarrow> \<sigma>\<^sub>1 = \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>to_ordered_collection \<tau> \<sigma>\<^sub>1; to_ordered_collection \<tau> \<sigma>\<^sub>2\<rbrakk> \<Longrightarrow> \<sigma>\<^sub>1 = \<sigma>\<^sub>2
[PROOF STEP]
by (induct rule: to_ordered_collection.induct; simp add: to_ordered_collection.simps)