case H
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (destruct (append s nil)) (destruct s)
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ append s nil = s
apply coinduction2 s
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (destruct (append s nil)) (destruct s)
case H
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (destruct (append s nil)) (destruct s)
intro s
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (destruct (append nil nil)) (destruct nil)

α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ ∀ (x : α) (s : Seq α),
    BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (destruct (append (cons x s) nil)) (destruct (cons x s))
case H
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (destruct (append s nil)) (destruct s)
apply recOn s _ _
no goals
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (destruct (append nil nil)) (destruct nil)
trivial
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (destruct (append (cons x s) nil)) (destruct (cons x s))
α : Type u
β : Type v
γ : Type w
s✝ s : Seq α
⊢ ∀ (x : α) (s : Seq α),
    BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (destruct (append (cons x s) nil)) (destruct (cons x s))
intro x s
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (some (x, append s nil)) (some (x, s))
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (destruct (append (cons x s) nil)) (destruct (cons x s))
rw [cons_append, destruct_cons, destruct_cons]
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ x = x ∧ ∃ s_1, append s nil = append s_1 nil ∧ s = s_1
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ BisimO (fun s1 s2 => ∃ s, s1 = append s nil ∧ s2 = s) (some (x, append s nil)) (some (x, s))
dsimp
no goals
α : Type u
β : Type v
γ : Type w
s✝¹ s✝ : Seq α
x : α
s : Seq α
⊢ x = x ∧ ∃ s_1, append s nil = append s_1 nil ∧ s = s_1
exact ⟨rfl, s, rfl, rfl⟩