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