simp_all[bind_fun]
case none
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
h1 : bind_fun m1 m2 n = some v
n' : Nat
h : n' ≥ n
h2 : Subtype.val m1 n = none
⊢ bind_fun m1 m2 n' = some v
no goals