case mk
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
p : s ~> a
h : ∃ a, a ∈ s
⊢ a ∈ s
α : Type u
β : Type v
γ : Type w
s : Computation α
h : Terminates s
a : α
p : s ~> a
⊢ a ∈ s
cases' h with h
case mk.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a ∈ s
case mk
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
p : s ~> a
h : ∃ a, a ∈ s
⊢ a ∈ s
cases' h with a' h
case mk.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a' ∈ s
case mk.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a ∈ s
rw [p h]
no goals
case mk.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a' ∈ s
exact h