simp [SeqLeft.seqLeft, Seq.seq]
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (SeqLeft.seqLeft t₁ fun x => t₂) = Seq.seq (Function.const R₂ <$> t₁) fun x => t₂
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (bind t₁ fun a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> t₁) fun y => bind t₂ (ret ∘ y)