[STATEMENT]
lemma empty_code [code]:
  "empty = Lazy_Sequence (\<lambda>_. None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lazy_Sequence.empty = Lazy_Sequence Map.empty
[PROOF STEP]
by (simp add: lazy_sequence_eq_iff)