cases h2 : m1.val n with
| none => simp_all[bind_fun]
| some x =>
  simp_all[bind_fun]
  have m1_n'_runs : m1.val n' = some x := m1.property n x h2 n' h
  have m2_n'_runs : (m2 x).val n' = some v := (m2 x).property n v h1 n' h
  simp[m1_n'_runs, m2_n'_runs]
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
h1 : bind_fun m1 m2 n = some v
n' : Nat
h : n' ≥ n
⊢ bind_fun m1 m2 n' = some v
no goals