α : Type u
β : Type v
γ : Type w
s t : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 =>
    ∃ s t, c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t)
α : Type u
β : Type v
γ : Type w
s t : WSeq α
⊢ destruct (append s t) = Computation.bind (destruct s) (destruct_append.aux t)
apply
  Computation.eq_of_bisim
    (fun c1 c2 =>
      ∃ s t, c1 = destruct (append s t) ∧ c2 = (destruct s).bind (destruct_append.aux t))
    _ ⟨s, t, rfl, rfl⟩
α : Type u
β : Type v
γ : Type w
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
h : ∃ s t, c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s t, c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t))
    (Computation.destruct c1) (Computation.destruct c2)
α : Type u
β : Type v
γ : Type w
s t : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 =>
    ∃ s t, c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t)
intro c1 c2 h
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s t, c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t))
    (Computation.destruct c1) (Computation.destruct c2)
α : Type u
β : Type v
γ : Type w
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
h : ∃ s t, c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s t, c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t))
    (Computation.destruct c1) (Computation.destruct c2)
rcases h with ⟨s, t, h⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s t, c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t))
    (Computation.destruct (destruct (append s t)))
    (Computation.destruct (Computation.bind (destruct s) (destruct_append.aux t)))
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s t, c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t))
    (Computation.destruct c1) (Computation.destruct c2)
rw [h.left, h.right]
case intro.intro.h1
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h✝ : c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t)
h : c1 = destruct (append nil t) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)
⊢ match Computation.destruct (destruct t), Computation.destruct (destruct t) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    ∃ s_1 t,
      s = destruct (append s_1 t) ∧
        s' =
          Computation.bind (destruct s_1) fun x =>
            match x with
            | none => destruct t
            | some (a, s) => Computation.pure (some (a, append s t))
  | x, x_1 => False

case intro.intro.h3
α : Type u
β : Type v
γ : Type w
s✝¹ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s✝ t : WSeq α
h✝ : c1 = destruct (append s✝ t) ∧ c2 = Computation.bind (destruct s✝) (destruct_append.aux t)
s : WSeq α
h : c1 = destruct (append (think s) t) ∧ c2 = Computation.bind (destruct (think s)) (destruct_append.aux t)
⊢ ∃ s_1 t_1,
    destruct (append s t) = destruct (append s_1 t_1) ∧
      (Computation.bind (destruct s) fun x =>
          match x with
          | none => destruct t
          | some (a, s) => Computation.pure (some (a, append s t))) =
        Computation.bind (destruct s_1) fun x =>
          match x with
          | none => destruct t_1
          | some (a, s) => Computation.pure (some (a, append s t_1))
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s t, c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t))
    (Computation.destruct (destruct (append s t)))
    (Computation.destruct (Computation.bind (destruct s) (destruct_append.aux t)))
induction' s using WSeq.recOn with a s s <;> simp
case intro.intro.h1.h3
α : Type u
β : Type v
γ : Type w
s✝ t✝¹ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t✝ : WSeq α
h✝² : c1 = destruct (append s t✝) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t✝)
h✝¹ : c1 = destruct (append nil t✝) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t✝)
t : WSeq α
h✝ : c1 = destruct (append s (think t)) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux (think t))
h : c1 = destruct (append nil (think t)) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux (think t))
⊢ ∃ s t_1,
    destruct t = destruct (append s t_1) ∧
      destruct t =
        Computation.bind (destruct s) fun x =>
          match x with
          | none => destruct t_1
          | some (a, s) => Computation.pure (some (a, append s t_1))
case intro.intro.h1
α : Type u
β : Type v
γ : Type w
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h✝ : c1 = destruct (append s t) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t)
h : c1 = destruct (append nil t) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)
⊢ match Computation.destruct (destruct t), Computation.destruct (destruct t) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    ∃ s_1 t,
      s = destruct (append s_1 t) ∧
        s' =
          Computation.bind (destruct s_1) fun x =>
            match x with
            | none => destruct t
            | some (a, s) => Computation.pure (some (a, append s t))
  | x, x_1 => False
induction' t using WSeq.recOn with b t t <;> simp
no goals
case intro.intro.h1.h3
α : Type u
β : Type v
γ : Type w
s✝ t✝¹ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t✝ : WSeq α
h✝² : c1 = destruct (append s t✝) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux t✝)
h✝¹ : c1 = destruct (append nil t✝) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t✝)
t : WSeq α
h✝ : c1 = destruct (append s (think t)) ∧ c2 = Computation.bind (destruct s) (destruct_append.aux (think t))
h : c1 = destruct (append nil (think t)) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux (think t))
⊢ ∃ s t_1,
    destruct t = destruct (append s t_1) ∧
      destruct t =
        Computation.bind (destruct s) fun x =>
          match x with
          | none => destruct t_1
          | some (a, s) => Computation.pure (some (a, append s t_1))
refine' ⟨nil, t, _, _⟩ <;> simp
no goals
case intro.intro.h3
α : Type u
β : Type v
γ : Type w
s✝¹ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s✝ t : WSeq α
h✝ : c1 = destruct (append s✝ t) ∧ c2 = Computation.bind (destruct s✝) (destruct_append.aux t)
s : WSeq α
h : c1 = destruct (append (think s) t) ∧ c2 = Computation.bind (destruct (think s)) (destruct_append.aux t)
⊢ ∃ s_1 t_1,
    destruct (append s t) = destruct (append s_1 t_1) ∧
      (Computation.bind (destruct s) fun x =>
          match x with
          | none => destruct t
          | some (a, s) => Computation.pure (some (a, append s t))) =
        Computation.bind (destruct s_1) fun x =>
          match x with
          | none => destruct t_1
          | some (a, s) => Computation.pure (some (a, append s t_1))
exact ⟨s, t, rfl, rfl⟩