case a
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
⊢ ↑s = ↑(empty α)
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
⊢ s = empty α
apply Subtype.eq
case a.h
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
n : ℕ
⊢ ↑s n = ↑(empty α) n
case a
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
⊢ ↑s = ↑(empty α)
funext n
case a.h.none
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
n : ℕ
x✝ : Option α
h✝ : ↑s n = x✝
h : ↑s n = none
⊢ none = ↑(empty α) n

case a.h.some
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
n : ℕ
x✝ : Option α
h✝ : ↑s n = x✝
val✝ : α
h : ↑s n = some val✝
⊢ some val✝ = ↑(empty α) n
case a.h
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
n : ℕ
⊢ ↑s n = ↑(empty α) n
induction' h : s.val n with _
case a.h.some
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
n : ℕ
x✝ : Option α
h✝ : ↑s n = x✝
val✝ : α
h : ↑s n = some val✝
⊢ Terminates s
case a.h.some
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
n : ℕ
x✝ : Option α
h✝ : ↑s n = x✝
val✝ : α
h : ↑s n = some val✝
⊢ some val✝ = ↑(empty α) n
refine' absurd _ H
no goals
case a.h.some
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
n : ℕ
x✝ : Option α
h✝ : ↑s n = x✝
val✝ : α
h : ↑s n = some val✝
⊢ Terminates s
exact ⟨⟨_, _, h.symm⟩⟩
no goals
case a.h.none
α : Type u
β : Type v
γ : Type w
s : Computation α
H : ¬Terminates s
n : ℕ
x✝ : Option α
h✝ : ↑s n = x✝
h : ↑s n = none
⊢ none = ↑(empty α) n
rfl