α : Type u
β : Type v
γ : Type w
c : Computation α
⊢ IsBisimulation fun c₁ c₂ => (HOrElse.hOrElse c₂ fun x => empty α) = c₁
α : Type u
β : Type v
γ : Type w
c : Computation α
⊢ (HOrElse.hOrElse c fun x => empty α) = c
apply eq_of_bisim (fun c₁ c₂ => (c₂ <|> empty α) = c₁) _ rfl
α : Type u
β : Type v
γ : Type w
c s' s : Computation α
h : (HOrElse.hOrElse s fun x => empty α) = s'
⊢ BisimO (fun c₁ c₂ => (HOrElse.hOrElse c₂ fun x => empty α) = c₁) (destruct s') (destruct s)
α : Type u
β : Type v
γ : Type w
c : Computation α
⊢ IsBisimulation fun c₁ c₂ => (HOrElse.hOrElse c₂ fun x => empty α) = c₁
intro s' s h
α : Type u
β : Type v
γ : Type w
c s' s : Computation α
h : (HOrElse.hOrElse s fun x => empty α) = s'
⊢ BisimO (fun c₁ c₂ => (HOrElse.hOrElse c₂ fun x => empty α) = c₁) (destruct (HOrElse.hOrElse s fun x => empty α))
    (destruct s)
α : Type u
β : Type v
γ : Type w
c s' s : Computation α
h : (HOrElse.hOrElse s fun x => empty α) = s'
⊢ BisimO (fun c₁ c₂ => (HOrElse.hOrElse c₂ fun x => empty α) = c₁) (destruct s') (destruct s)
rw [← h]
case h2
α : Type u
β : Type v
γ : Type w
c s' s✝ : Computation α
h : (HOrElse.hOrElse s✝ fun x => empty α) = s'
s : Computation α
⊢ (HOrElse.hOrElse s fun x => think (empty α)) = HOrElse.hOrElse s fun x => empty α
α : Type u
β : Type v
γ : Type w
c s' s : Computation α
h : (HOrElse.hOrElse s fun x => empty α) = s'
⊢ BisimO (fun c₁ c₂ => (HOrElse.hOrElse c₂ fun x => empty α) = c₁) (destruct (HOrElse.hOrElse s fun x => empty α))
    (destruct s)
apply recOn s <;> intro s <;> rw [think_empty] <;> simp
no goals
case h2
α : Type u
β : Type v
γ : Type w
c s' s✝ : Computation α
h : (HOrElse.hOrElse s✝ fun x => empty α) = s'
s : Computation α
⊢ (HOrElse.hOrElse s fun x => think (empty α)) = HOrElse.hOrElse s fun x => empty α
rw [← think_empty]