[STATEMENT]
lemma lmap_Lazy_llist [code]:
  "lmap f (Lazy_llist xs) = Lazy_llist (\<lambda>_. map_option (map_prod f (lmap f)) (xs ()))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmap f (Lazy_llist xs) = Lazy_llist (\<lambda>_. map_option (map_prod f (lmap f)) (xs ()))
[PROOF STEP]
by simp