simp [ih, h]
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)
h : ∀ (x y z : String), x ++ (y ++ z) = x ++ y ++ z
⊢ (bind (h✝ T✝ e✝) fun x => bind (interp h✝ (bind (k✝ x.fst) k)) fun y => ret (y.fst, x.snd ++ y.snd)) =
    bind (h✝ T✝ e✝) fun x =>
      bind (interp h✝ (k✝ x.fst)) fun x_1 =>
        bind (interp h✝ (k x_1.fst)) fun x_2 => ret (x_2.fst, x.snd ++ x_1.snd ++ x_2.snd)
no goals