case bisim
α : Type u
β : Type v
γ : Type w
s : Computation α
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s

case r
α : Type u
β : Type v
γ : Type w
s : Computation α
⊢ bind s pure = s ∨ ∃ s_1, bind s pure = bind s_1 pure ∧ s = s_1
α : Type u
β : Type v
γ : Type w
s : Computation α
⊢ bind s pure = s
apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure) ∧ c₂ = s
case r
α : Type u
β : Type v
γ : Type w
s : Computation α
⊢ bind s pure = s ∨ ∃ s_1, bind s pure = bind s_1 pure ∧ s = s_1
case bisim
α : Type u
β : Type v
γ : Type w
s : Computation α
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s

case r
α : Type u
β : Type v
γ : Type w
s : Computation α
⊢ bind s pure = s ∨ ∃ s_1, bind s pure = bind s_1 pure ∧ s = s_1
. intro c₁ c₂ h
  exact
    match c₁, c₂, h with
    | _, c₂, Or.inl (Eq.refl _) => by cases' destruct c₂ with b cb <;> simp
    | _, _, Or.inr ⟨s, rfl, rfl⟩ => by
      apply recOn s <;> intro s <;> simp
no goals
case r
α : Type u
β : Type v
γ : Type w
s : Computation α
⊢ bind s pure = s ∨ ∃ s_1, bind s pure = bind s_1 pure ∧ s = s_1
. exact Or.inr ⟨s, rfl, rfl⟩
case bisim
α : Type u
β : Type v
γ : Type w
s c₁ c₂ : Computation α
h : c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s) (destruct c₁) (destruct c₂)
case bisim
α : Type u
β : Type v
γ : Type w
s : Computation α
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s
intro c₁ c₂ h
no goals
case bisim
α : Type u
β : Type v
γ : Type w
s c₁ c₂ : Computation α
h : c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s) (destruct c₁) (destruct c₂)
exact
  match c₁, c₂, h with
  | _, c₂, Or.inl (Eq.refl _) => by cases' destruct c₂ with b cb <;> simp
  | _, _, Or.inr ⟨s, rfl, rfl⟩ => by
    apply recOn s <;> intro s <;> simp
no goals
α : Type u
β : Type v
γ : Type w
s c₁ c₂✝ : Computation α
h : c₁ = c₂✝ ∨ ∃ s, c₁ = bind s pure ∧ c₂✝ = s
c₂ : Computation α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s) (destruct c₂) (destruct c₂)
cases' destruct c₂ with b cb <;> simp
no goals
α : Type u
β : Type v
γ : Type w
s✝ c₁ c₂ : Computation α
h : c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s
s : Computation α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s) (destruct (bind s pure)) (destruct s)
apply recOn s <;> intro s <;> simp
no goals
case r
α : Type u
β : Type v
γ : Type w
s : Computation α
⊢ bind s pure = s ∨ ∃ s_1, bind s pure = bind s_1 pure ∧ s = s_1
exact Or.inr ⟨s, rfl, rfl⟩