α : Type u
β : Type v
γ : Type w
⊢ ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o : Option α}, o ∈ head s → o ∈ head t
α : Type u
β : Type v
γ : Type w
⊢ ∀ {s t : WSeq α}, s ~ʷ t → head s ~ head t
suffices ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o}, o ∈ head s → o ∈ head t from fun s t h o =>
  ⟨this h, this h.symm⟩
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
⊢ o ∈ head t
α : Type u
β : Type v
γ : Type w
⊢ ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o : Option α}, o ∈ head s → o ∈ head t
intro s t h o ho
case intro.intro
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
ds : Option (α × WSeq α)
dsm : ds ∈ destruct s
dse : Prod.fst <$> ds = o
⊢ o ∈ head t
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
⊢ o ∈ head t
rcases @Computation.exists_of_mem_map _ _ _ _ (destruct s) ho with ⟨ds, dsm, dse⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
ds : Option (α × WSeq α)
dsm : ds ∈ destruct s
dse : Prod.fst <$> ds = o
⊢ Prod.fst <$> ds ∈ head t
case intro.intro
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
ds : Option (α × WSeq α)
dsm : ds ∈ destruct s
dse : Prod.fst <$> ds = o
⊢ o ∈ head t
rw [← dse]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
ds : Option (α × WSeq α)
dsm : ds ∈ destruct s
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
⊢ Prod.fst <$> ds ∈ head t
case intro.intro
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
ds : Option (α × WSeq α)
dsm : ds ∈ destruct s
dse : Prod.fst <$> ds = o
⊢ Prod.fst <$> ds ∈ head t
cases' destruct_congr h with l r
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
ds : Option (α × WSeq α)
dsm : ds ∈ destruct s
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
dt : Option (α × WSeq α)
dtm : dt ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) ds dt
⊢ Prod.fst <$> ds ∈ head t
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
ds : Option (α × WSeq α)
dsm : ds ∈ destruct s
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
⊢ Prod.fst <$> ds ∈ head t
rcases l dsm with ⟨dt, dtm, dst⟩
case intro.intro.intro.intro.intro.none.none
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
dsm : none ∈ destruct s
dse : Prod.fst <$> none = o
dtm : none ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) none none
⊢ Prod.fst <$> none ∈ head t

case intro.intro.intro.intro.intro.none.some
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
dsm : none ∈ destruct s
dse : Prod.fst <$> none = o
b : α × WSeq α
dtm : some b ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) none (some b)
⊢ Prod.fst <$> none ∈ head t

case intro.intro.intro.intro.intro.some.none
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
a : α × WSeq α
dsm : some a ∈ destruct s
dse : Prod.fst <$> some a = o
dtm : none ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some a) none
⊢ Prod.fst <$> some a ∈ head t

case intro.intro.intro.intro.intro.some.some
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
a : α × WSeq α
dsm : some a ∈ destruct s
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some a) (some b)
⊢ Prod.fst <$> some a ∈ head t
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
ds : Option (α × WSeq α)
dsm : ds ∈ destruct s
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
dt : Option (α × WSeq α)
dtm : dt ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) ds dt
⊢ Prod.fst <$> ds ∈ head t
cases' ds with a <;> cases' dt with b
no goals
case intro.intro.intro.intro.intro.none.none
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
dsm : none ∈ destruct s
dse : Prod.fst <$> none = o
dtm : none ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) none none
⊢ Prod.fst <$> none ∈ head t
apply Computation.mem_map _ dtm
case intro.intro.intro.intro.intro.none.some.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
dsm : none ∈ destruct s
dse : Prod.fst <$> none = o
fst✝ : α
snd✝ : WSeq α
dtm : some (fst✝, snd✝) ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) none (some (fst✝, snd✝))
⊢ Prod.fst <$> none ∈ head t
case intro.intro.intro.intro.intro.none.some
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
dsm : none ∈ destruct s
dse : Prod.fst <$> none = o
b : α × WSeq α
dtm : some b ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) none (some b)
⊢ Prod.fst <$> none ∈ head t
cases b
no goals
case intro.intro.intro.intro.intro.none.some.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
dsm : none ∈ destruct s
dse : Prod.fst <$> none = o
fst✝ : α
snd✝ : WSeq α
dtm : some (fst✝, snd✝) ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) none (some (fst✝, snd✝))
⊢ Prod.fst <$> none ∈ head t
cases dst
case intro.intro.intro.intro.intro.some.none.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
dtm : none ∈ destruct t
fst✝ : α
snd✝ : WSeq α
dsm : some (fst✝, snd✝) ∈ destruct s
dse : Prod.fst <$> some (fst✝, snd✝) = o
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some (fst✝, snd✝)) none
⊢ Prod.fst <$> some (fst✝, snd✝) ∈ head t
case intro.intro.intro.intro.intro.some.none
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
a : α × WSeq α
dsm : some a ∈ destruct s
dse : Prod.fst <$> some a = o
dtm : none ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some a) none
⊢ Prod.fst <$> some a ∈ head t
cases a
no goals
case intro.intro.intro.intro.intro.some.none.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
dtm : none ∈ destruct t
fst✝ : α
snd✝ : WSeq α
dsm : some (fst✝, snd✝) ∈ destruct s
dse : Prod.fst <$> some (fst✝, snd✝) = o
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some (fst✝, snd✝)) none
⊢ Prod.fst <$> some (fst✝, snd✝) ∈ head t
cases dst
case intro.intro.intro.intro.intro.some.some.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
b : α × WSeq α
dtm : some b ∈ destruct t
a : α
s' : WSeq α
dsm : some (a, s') ∈ destruct s
dse : Prod.fst <$> some (a, s') = o
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some (a, s')) (some b)
⊢ Prod.fst <$> some (a, s') ∈ head t
case intro.intro.intro.intro.intro.some.some
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
a : α × WSeq α
dsm : some a ∈ destruct s
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some a) (some b)
⊢ Prod.fst <$> some a ∈ head t
cases' a with a s'
case intro.intro.intro.intro.intro.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ destruct s
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (a, s') ∈ head t
case intro.intro.intro.intro.intro.some.some.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
b : α × WSeq α
dtm : some b ∈ destruct t
a : α
s' : WSeq α
dsm : some (a, s') ∈ destruct s
dse : Prod.fst <$> some (a, s') = o
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some (a, s')) (some b)
⊢ Prod.fst <$> some (a, s') ∈ head t
cases' b with b t'
case intro.intro.intro.intro.intro.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ destruct s
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (b, s') ∈ head t
case intro.intro.intro.intro.intro.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ destruct s
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (a, s') ∈ head t
rw [dst.left]
no goals
case intro.intro.intro.intro.intro.some.some.mk.mk
α : Type u
β : Type v
γ : Type w
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ head s
l : ∀ {a : Option (α × WSeq α)}, a ∈ destruct s → ∃ b, b ∈ destruct t ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ destruct t → ∃ a, a ∈ destruct s ∧ BisimO (fun x x_1 => x ~ʷ x_1) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ destruct s
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ destruct t
dst : BisimO (fun x x_1 => x ~ʷ x_1) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (b, s') ∈ head t
exact @Computation.mem_map _ _ (@Functor.map _ _ (α × WSeq α) _ Prod.fst)
  (some (b, t')) (destruct t) dtm