case nil
α : Type u_1
⊢ append nil (Thunk.pure nil) = nil

case cons
α : Type u_1
xs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.62837 tl✝
⊢ append (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝

case mk
α : Type u_1
xs : LazyList α
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a
⊢ ?m.62837 { fn := fn✝ }
α : Type u_1
xs : LazyList α
⊢ append xs (Thunk.pure nil) = xs
induction' xs using LazyList.rec with _ _ _ _ ih
no goals
case nil
α : Type u_1
⊢ append nil (Thunk.pure nil) = nil
rfl
no goals
case cons
α : Type u_1
xs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.62837 tl✝
⊢ append (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝
simpa only [append, cons.injEq, true_and]
case mk.eq
α : Type u_1
xs : LazyList α
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a
⊢ Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = Thunk.get { fn := fn✝ }
case mk
α : Type u_1
xs : LazyList α
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a
⊢ { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = { fn := fn✝ }
ext
no goals
case mk.eq
α : Type u_1
xs : LazyList α
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a
⊢ Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = Thunk.get { fn := fn✝ }
apply ih