simp [HAppend.hAppend, Append.append, String.append]
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)
⊢ ∀ (x y z : String), x ++ (y ++ z) = x ++ y ++ z
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)
⊢ ∀ (x y z : String), { data := x.data ++ (y.data ++ z.data) } = { data := x.data ++ y.data ++ z.data }