α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
⊢ ∀ (b : Option α) (s' : Seq (Option α)), some a = b ∨ C s' → C (Seq.cons b s')
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
⊢ C s
apply Seq.mem_rec_on M
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
o : Option α
s' : Seq (Option α)
h : some a = o ∨ C s'
⊢ C (Seq.cons o s')
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
⊢ ∀ (b : Option α) (s' : Seq (Option α)), some a = b ∨ C s' → C (Seq.cons b s')
intro o s' h
case none
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
h : some a = none ∨ C s'
⊢ C (Seq.cons none s')

case some
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ C (Seq.cons (some b) s')
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
o : Option α
s' : Seq (Option α)
h : some a = o ∨ C s'
⊢ C (Seq.cons o s')
cases' o with b
case none.a
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
h : some a = none ∨ C s'
⊢ C s'
case none
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
h : some a = none ∨ C s'
⊢ C (Seq.cons none s')
apply h2
case none.a.inl
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
h✝ : some a = none
⊢ C s'

case none.a.inr
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
h✝ : C s'
⊢ C s'
case none.a
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
h : some a = none ∨ C s'
⊢ C s'
cases h
no goals
case none.a.inl
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
h✝ : some a = none
⊢ C s'
contradiction
no goals
case none.a.inr
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
h✝ : C s'
⊢ C s'
assumption
case some.a
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ a = b ∨ C s'
case some
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ C (Seq.cons (some b) s')
apply h1
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ some a = some b → a = b
case some.a
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ a = b ∨ C s'
apply Or.imp_left _ h
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
b : α
h✝ : some a = some b ∨ C s'
h : some a = some b
⊢ a = b
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ some a = some b → a = b
intro h
no goals
α : Type u
β : Type v
γ : Type w
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C (think s)
s' : Seq (Option α)
b : α
h✝ : some a = some b ∨ C s'
h : some a = some b
⊢ a = b
injection h