induction n with
| zero => simp_all_arith[fix', bottom]
| succ m ih =>
  simp_all[fix', runTo]
  sorry
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
steps n : Nat
x : α
v : β
h1 : Subtype.val (fix' f n x) steps = some v
n' : Nat
h2 : n' ≥ n
⊢ Subtype.val (fix' f n' x) steps = some v
no goals