have fequal2 α β (f g: α → β) x y: f = g → x = y → f x = g y :=
  fun h₁ h₂ => by simp [h₁, h₂]
case Vis
E F : Type → Type
T R : Type
h : E ~> OptionT (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? =>
        match x? with
        | some x => interp h (k x)
        | none => ret none
⊢ (bind (h T✝ e✝) fun __do_lift =>
      match __do_lift with
      | some a => interp h (bind (k✝ a) k)
      | none => ret none) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | some a => interp h (k✝ a)
        | none => ret none)
        fun x? =>
        match x? with
        | some x => interp h (k x)
        | none => ret none
case Vis
E F : Type → Type
T R : Type
h : E ~> OptionT (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? =>
        match x? with
        | some x => interp h (k x)
        | none => ret none
fequal2 : ∀ (α : Sort ?u.47259) (β : Sort ?u.47260) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (bind (h T✝ e✝) fun __do_lift =>
      match __do_lift with
      | some a => interp h (bind (k✝ a) k)
      | none => ret none) =
    bind (h T✝ e✝) fun x =>
      bind
        (match x with
        | some a => interp h (k✝ a)
        | none => ret none)
        fun x? =>
        match x? with
        | some x => interp h (k x)
        | none => ret none