α : Type u
β : Type v
S : WSeq (Computation α)
a : α
H : ∀ (s : Computation α), s ∈ S → s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this : Terminates c
⊢ a ∈ parallel S
α : Type u
β : Type v
S : WSeq (Computation α)
a : α
H : ∀ (s : Computation α), s ∈ S → s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
⊢ a ∈ parallel S
haveI := terminates_of_mem ac
α : Type u
β : Type v
S : WSeq (Computation α)
a : α
H : ∀ (s : Computation α), s ∈ S → s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this✝ : Terminates c
this : Terminates (parallel S)
⊢ a ∈ parallel S
α : Type u
β : Type v
S : WSeq (Computation α)
a : α
H : ∀ (s : Computation α), s ∈ S → s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this : Terminates c
⊢ a ∈ parallel S
haveI := terminates_parallel cs
no goals
α : Type u
β : Type v
S : WSeq (Computation α)
a : α
H : ∀ (s : Computation α), s ∈ S → s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this✝ : Terminates c
this : Terminates (parallel S)
⊢ a ∈ parallel S
exact mem_of_promises _ (parallel_promises H)