α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (tail s))
⊢ ∃ a', some a' ∈ head s
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : some a ∈ head (tail s)
⊢ ∃ a', some a' ∈ head s
unfold head at h
case intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (tail s))
o : Option (α × WSeq α)
md : o ∈ destruct (tail s)
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ head s
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (tail s))
⊢ ∃ a', some a' ∈ head s
rcases Computation.exists_of_mem_map h with ⟨o, md, e⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ destruct (tail s)
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ head s
case intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (tail s))
o : Option (α × WSeq α)
md : o ∈ destruct (tail s)
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ head s
clear h
case intro.intro.some
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ destruct (tail s)
h' : o.fst = a
⊢ ∃ a', some a' ∈ head s
case intro.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ destruct (tail s)
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ head s
cases' o with o <;> [injection e; injection e with h']
case intro.intro.some
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ destruct (tail s)
⊢ ∃ a', some a' ∈ head s
case intro.intro.some
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ destruct (tail s)
h' : o.fst = a
⊢ ∃ a', some a' ∈ head s
clear h'
case intro.intro.some.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a✝ : α
o : α × WSeq α
md : some o ∈ destruct (tail s)
a : α × WSeq α
am : some a ∈ destruct s
⊢ ∃ a', some a' ∈ head s
case intro.intro.some
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ destruct (tail s)
⊢ ∃ a', some a' ∈ head s
cases' destruct_some_of_destruct_tail_some md with a am