α : Type u
β : Type v
γ : Type w
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : destruct s = c
⊢ some (a', s') ∈ c → (a ∈ s ↔ a = a' ∨ a ∈ s')
α : Type u
β : Type v
γ : Type w
s : WSeq α
a a' : α
s' : WSeq α
⊢ some (a', s') ∈ destruct s → (a ∈ s ↔ a = a' ∨ a ∈ s')
generalize e : destruct s = c
α : Type u
β : Type v
γ : Type w
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : destruct s = c
h : some (a', s') ∈ c
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'
α : Type u
β : Type v
γ : Type w
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : destruct s = c
⊢ some (a', s') ∈ c → (a ∈ s ↔ a = a' ∨ a ∈ s')
intro h
α : Type u
β : Type v
γ : Type w
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
⊢ ∀ {s : WSeq α}, destruct s = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
α : Type u
β : Type v
γ : Type w
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : destruct s = c
h : some (a', s') ∈ c
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'
revert s
case h1.h2
α : Type u
β : Type v
γ : Type w
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : destruct (cons x s) = Computation.pure (some (a', s'))
this : x = a' ∧ s = s'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'

case h2.h3
α : Type u
β : Type v
γ : Type w
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, destruct s = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s : WSeq α
m : destruct (think s) = Computation.think c
this : destruct s = c
⊢ a ∈ think s ↔ a = a' ∨ a ∈ s'
α : Type u
β : Type v
γ : Type w
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
⊢ ∀ {s : WSeq α}, destruct s = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
apply Computation.memRecOn h <;> [skip; intro c IH] <;> intro s <;>
  induction' s using WSeq.recOn with x s s <;>
  intro m <;>
  have := congr_arg Computation.destruct m <;>
  simp at this
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : destruct (cons x s) = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'
case h1.h2
α : Type u
β : Type v
γ : Type w
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : destruct (cons x s) = Computation.pure (some (a', s'))
this : x = a' ∧ s = s'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'
cases' this with i1 i2
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : destruct (cons x s) = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ a ∈ cons a' s' ↔ a = a' ∨ a ∈ s'
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : destruct (cons x s) = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'
rw [i1, i2]
case h1.h2.intro.mk
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
⊢ a ∈ cons a' { val := f, property := al } ↔ a = a' ∨ a ∈ { val := f, property := al }
case h1.h2.intro
α : Type u
β : Type v
γ : Type w
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : destruct (cons x s) = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ a ∈ cons a' s' ↔ a = a' ∨ a ∈ s'
cases' s' with f al
case h1.h2.intro.mk
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
⊢ Any (fun b => some (some a) = b) (some (some a') :: f) ↔ a = a' ∨ Any (fun b => some (some a) = b) f
case h1.h2.intro.mk
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
⊢ Any (fun b => some (some a) = b) (some (some a') :: f) ↔ a = a' ∨ Any (fun b => some (some a) = b) f
have h_a_eq_a' : a = a' ↔ some (some a) = some (some a') := by simp
case h1.h2.intro.mk
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
⊢ Any (fun b => some (some a) = b) (some (some a') :: f) ↔
    some (some a) = some (some a') ∨ Any (fun b => some (some a) = b) f
case h1.h2.intro.mk
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
⊢ Any (fun b => some (some a) = b) (some (some a') :: f) ↔ a = a' ∨ Any (fun b => some (some a) = b) f
rw [h_a_eq_a']
case h1.h2.intro.mk
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
o : some (some a) = some (some a') ∨ Any (fun b => some (some a) = b) f
⊢ Any (fun b => some (some a) = b) (some (some a') :: f)
case h1.h2.intro.mk
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
⊢ Any (fun b => some (some a) = b) (some (some a') :: f) ↔
    some (some a) = some (some a') ∨ Any (fun b => some (some a) = b) f
refine' ⟨Stream'.eq_or_mem_of_mem_cons, fun o => _⟩
no goals
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
⊢ a = a' ↔ some (some a) = some (some a')
simp
case h1.h2.intro.mk.inl
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
e : some (some a) = some (some a')
⊢ Any (fun b => some (some a) = b) (some (some a') :: f)

case h1.h2.intro.mk.inr
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m✝ : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
m : Any (fun b => some (some a) = b) f
⊢ Any (fun b => some (some a) = b) (some (some a') :: f)
case h1.h2.intro.mk
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
o : some (some a) = some (some a') ∨ Any (fun b => some (some a) = b) f
⊢ Any (fun b => some (some a) = b) (some (some a') :: f)
cases' o with e m
case h1.h2.intro.mk.inl
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
e : some (some a) = some (some a')
⊢ Any (fun b => some (some a') = b) (some (some a') :: f)
case h1.h2.intro.mk.inl
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
e : some (some a) = some (some a')
⊢ Any (fun b => some (some a) = b) (some (some a') :: f)
rw [e]
no goals
case h1.h2.intro.mk.inl
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
e : some (some a) = some (some a')
⊢ Any (fun b => some (some a') = b) (some (some a') :: f)
apply Stream'.mem_cons
no goals
case h1.h2.intro.mk.inr
α : Type u
β : Type v
γ : Type w
a a' : α
c : Computation (Option (α × WSeq α))
x : α
s : WSeq α
i1 : x = a'
f : Stream' (Option (Option α))
al : IsSeq f
h : some (a', { val := f, property := al }) ∈ c
m✝ : destruct (cons x s) = Computation.pure (some (a', { val := f, property := al }))
i2 : s = { val := f, property := al }
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
m : Any (fun b => some (some a) = b) f
⊢ Any (fun b => some (some a) = b) (some (some a') :: f)
exact Stream'.mem_cons_of_mem _ m
no goals
case h2.h3
α : Type u
β : Type v
γ : Type w
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, destruct s = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s : WSeq α
m : destruct (think s) = Computation.think c
this : destruct s = c
⊢ a ∈ think s ↔ a = a' ∨ a ∈ s'
simp [IH this]