simp [interpWriter] at *
case Vis
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interpWriter h (bind (k✝ a) k) =
      bind (interpWriter h (k✝ a)) fun x =>
        match x with
        | (x, s₁) =>
          bind (interpWriter h (k x)) fun x =>
            match x with
            | (y, s₂) => ret (y, s₁ ++ s₂)
⊢ interpWriter h (bind (Vis e✝ k✝) k) =
    bind (interpWriter h (Vis e✝ k✝)) fun x =>
      match x with
      | (x, s₁) =>
        bind (interpWriter h (k x)) fun x =>
          match x with
          | (y, s₂) => ret (y, s₁ ++ s₂)
case Vis
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E T
ih :
  ∀ (a : T✝),
    interp h (bind (k✝ a) k) =
      bind (interp h (k✝ a)) fun x => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)
⊢ interp h (bind (Vis e✝ k✝) k) =
    bind (interp h (Vis e✝ k✝)) fun x => bind (interp h (k x.fst)) fun x_1 => ret (x_1.fst, x.snd ++ x_1.snd)