sorry
case intro.v1
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β
no goals