simp [HAppend.hAppend, Append.append, String.append]
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ ∀ (x : String), "" ++ x = x
E F : Type → Type
T R : Type
h : E ~> WriterT (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ ∀ (x : String), { data := [] ++ x.data } = x