α : Type u
β : Type v
γ : Type w
s : Computation α
T : Terminates s
a : α
h : a ∈ s
⊢ Results s (get s) (length s)
α : Type u
β : Type v
γ : Type w
s : Computation α
T : Terminates s
a : α
h : a ∈ s
⊢ Results s a (length s)
rw [← get_eq_of_mem _ h]
no goals
α : Type u
β : Type v
γ : Type w
s : Computation α
T : Terminates s
a : α
h : a ∈ s
⊢ Results s (get s) (length s)
apply results_of_terminates