case H
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ ∀ (s : Seq α),
    BisimO (fun s1 s2 => ∃ s, s1 = Seq.join (Seq.map ret s) ∧ s2 = s) (destruct (Seq.join (Seq.map ret s))) (destruct s)
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ Seq.join (Seq.map ret s) = s
apply coinduction2 s
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = Seq.join (Seq.map ret s) ∧ s2 = s) (destruct (Seq.join (Seq.map ret s))) (destruct s)
case H
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ ∀ (s : Seq α),
    BisimO (fun s1 s2 => ∃ s, s1 = Seq.join (Seq.map ret s) ∧ s2 = s) (destruct (Seq.join (Seq.map ret s))) (destruct s)
intro s
no goals
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = Seq.join (Seq.map ret s) ∧ s2 = s) (destruct (Seq.join (Seq.map ret s))) (destruct s)
apply recOn s <;> simp [ret]