[STATEMENT]
lemma mkt_stocks_assets:
  shows "stk_strict_subs (stocks Mkt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stk_strict_subs (stocks Mkt)
[PROOF STEP]
unfolding stocks_def prices_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stk_strict_subs (fst (Rep_discrete_market Mkt))
[PROOF STEP]
by (metis Rep_discrete_market mem_Collect_eq split_beta')