induction t with
| Ret _ =>
    simp [bind, interpWriter]
    have h₁: forall x, "" ++ x = x := by
      simp [HAppend.hAppend, Append.append, String.append]
      simp [List.nil_append]
    simp [h₁]
    have h₂: forall (α β: Type) (x: α × β), (x.fst, x.snd) = x := by simp
    simp [h₂]
| Vis _ _ ih =>
    simp [interpWriter] at *
    simp [interp, Bind.bind, WriterT.bindCont, WriterT.mk]
    have h: forall (x y z: String), x ++ (y ++ z) = x ++ y ++ z := by
      simp [HAppend.hAppend, Append.append, String.append]
      simp [List.append_assoc]
    simp [ih, h]
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
t : Fitree E T
k : T → Fitree E R
⊢ interpWriter h (bind t k) =
    bind (interpWriter h t) fun x =>
      match x with
      | (x, s₁) =>
        bind (interpWriter h (k x)) fun x =>
          match x with
          | (y, s₂) => ret (y, s₁ ++ s₂)
no goals