sorry
case succ
α β : Type
f : (α → Computation β) → α → Computation β
steps : Nat
x : α
v : β
n' m : Nat
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    Subtype.val (f v1 x) n = some v →
      ∀ (v2 : α → Computation β),
        (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → Subtype.val (f v2 x) n = some v
ih : Subtype.val (fix' f m x) steps = some v → n' ≥ m → Subtype.val (fix' f n' x) steps = some v
h1 : Subtype.val (f (fix' f m) x) steps = some v
h2 : n' ≥ Nat.succ m
⊢ Subtype.val (fix' f n' x) steps = some v
no goals