[STATEMENT]
lemma sorted_sorted_domain: "sorted_wrt (lt ko) (sorted_domain ko xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (lt ko) (sorted_domain ko xs)
[PROOF STEP]
unfolding sorted_domain_def lt_of_key_order.rep_eq[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (lt_of_key_order (rep_key_order ko)) (sorted_domain_raw ko (list_of_oalist xs))
[PROOF STEP]
using oalist_inv_list_of_oalist
[PROOF STATE]
proof (prove)
using this:
oalist_inv (list_of_oalist ?x)

goal (1 subgoal):
 1. sorted_wrt (lt_of_key_order (rep_key_order ko)) (sorted_domain_raw ko (list_of_oalist xs))
[PROOF STEP]
by (rule sorted_sorted_domain_raw)