α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
⊢ destruct (flatten c) = c >>= destruct
refine'
  Computation.eq_of_bisim
    (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct) _
    (Or.inr ⟨c, rfl, rfl⟩)
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct)
    (Computation.destruct c1) (Computation.destruct c2)
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct
intro c1 c2 h
no goals
α : Type u
β : Type v
γ : Type w
c✝ : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct
c : Computation (Option (α × WSeq α))
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct)
    (Computation.destruct c) (Computation.destruct c)
cases c.destruct <;> simp
case h1
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct
a : WSeq α
⊢ match Computation.destruct (destruct a), Computation.destruct (destruct a) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = destruct (flatten c) ∧ s' = Computation.bind c destruct
  | x, x_1 => False

case h2
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct
c' : Computation (WSeq α)
⊢ destruct (flatten c') = Computation.bind c' destruct ∨
    ∃ c, destruct (flatten c') = destruct (flatten c) ∧ Computation.bind c' destruct = Computation.bind c destruct
α : Type u
β : Type v
γ : Type w
c✝ : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct
c : Computation (WSeq α)
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct)
    (Computation.destruct (destruct (flatten c))) (Computation.destruct (Computation.bind c destruct))
induction' c using Computation.recOn with a c' <;> simp
no goals
case h1
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct
a : WSeq α
⊢ match Computation.destruct (destruct a), Computation.destruct (destruct a) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = destruct (flatten c) ∧ s' = Computation.bind c destruct
  | x, x_1 => False
cases (destruct a).destruct <;> simp
no goals
case h2
α : Type u
β : Type v
γ : Type w
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct
c' : Computation (WSeq α)
⊢ destruct (flatten c') = Computation.bind c' destruct ∨
    ∃ c, destruct (flatten c') = destruct (flatten c) ∧ Computation.bind c' destruct = Computation.bind c destruct
exact Or.inr ⟨c', rfl, rfl⟩