case bisim
α : Type u
β : Type v
γ : Type w
s t u : Seq α
⊢ IsBisimulation fun s1 s2 => ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)

case r
α : Type u
β : Type v
γ : Type w
s t u : Seq α
⊢ ∃ s_1 t_1 u_1,
    append (append s t) u = append (append s_1 t_1) u_1 ∧ append s (append t u) = append s_1 (append t_1 u_1)
α : Type u
β : Type v
γ : Type w
s t u : Seq α
⊢ append (append s t) u = append s (append t u)
apply eq_of_bisim fun s1 s2 => ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
case bisim
α : Type u
β : Type v
γ : Type w
s t u s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
⊢ BisimO (fun s1 s2 => ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)) (destruct s1) (destruct s2)
case bisim
α : Type u
β : Type v
γ : Type w
s t u : Seq α
⊢ IsBisimulation fun s1 s2 => ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
intro s1 s2 h
case h1
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ match destruct (append t u), destruct (append t u) with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t u, s = append (append s_1 t) u ∧ s' = append s_1 (append t u)
  | x, x_1 => False

case h2
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ α →
    ∀ (s : Seq α),
      ∃ s_1 t_1 u_1,
        append (append s t) u = append (append s_1 t_1) u_1 ∧ append s (append t u) = append s_1 (append t_1 u_1)
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ BisimO (fun s1 s2 => ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u))
    (destruct (append (append s t) u)) (destruct (append s (append t u)))
apply recOn s <;> simp
case h1.h1
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ match destruct u, destruct u with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t u, s = append (append s_1 t) u ∧ s' = append s_1 (append t u)
  | x, x_1 => False

case h1.h2
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ α → ∀ (s : Seq α), ∃ s_1 t u_1, append s u = append (append s_1 t) u_1 ∧ append s u = append s_1 (append t u_1)
case h1
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ match destruct (append t u), destruct (append t u) with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t u, s = append (append s_1 t) u ∧ s' = append s_1 (append t u)
  | x, x_1 => False
apply recOn t <;> simp
case h1.h1.h2
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ α → ∀ (s : Seq α), ∃ s_1 t u, s = append (append s_1 t) u ∧ s = append s_1 (append t u)
case h1.h1
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ match destruct u, destruct u with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t u, s = append (append s_1 t) u ∧ s' = append s_1 (append t u)
  | x, x_1 => False
apply recOn u <;> simp
case h1.h1.h2
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝¹ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ ∃ s t u_1, u = append (append s t) u_1 ∧ u = append s (append t u_1)
case h1.h1.h2
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ α → ∀ (s : Seq α), ∃ s_1 t u, s = append (append s_1 t) u ∧ s = append s_1 (append t u)
intro _ u
no goals
case h1.h1.h2
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝¹ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ ∃ s t u_1, u = append (append s t) u_1 ∧ u = append s (append t u_1)
refine' ⟨nil, nil, u, _, _⟩ <;> simp
case h1.h2
α : Type u
β : Type v
γ : Type w
s✝ t✝¹ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t✝ u : Seq α
x✝ : α
t : Seq α
⊢ ∃ s t_1 u_1, append t u = append (append s t_1) u_1 ∧ append t u = append s (append t_1 u_1)
case h1.h2
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ α → ∀ (s : Seq α), ∃ s_1 t u_1, append s u = append (append s_1 t) u_1 ∧ append s u = append s_1 (append t u_1)
intro _ t
no goals
case h1.h2
α : Type u
β : Type v
γ : Type w
s✝ t✝¹ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t✝ u : Seq α
x✝ : α
t : Seq α
⊢ ∃ s t_1 u_1, append t u = append (append s t_1) u_1 ∧ append t u = append s (append t_1 u_1)
refine' ⟨nil, t, u, _, _⟩ <;> simp
case h2
α : Type u
β : Type v
γ : Type w
s✝¹ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s✝ t u : Seq α
x✝ : α
s : Seq α
⊢ ∃ s_1 t_1 u_1,
    append (append s t) u = append (append s_1 t_1) u_1 ∧ append s (append t u) = append s_1 (append t_1 u_1)
case h2
α : Type u
β : Type v
γ : Type w
s✝ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s t u : Seq α
⊢ α →
    ∀ (s : Seq α),
      ∃ s_1 t_1 u_1,
        append (append s t) u = append (append s_1 t_1) u_1 ∧ append s (append t u) = append s_1 (append t_1 u_1)
intro _ s
no goals
case h2
α : Type u
β : Type v
γ : Type w
s✝¹ t✝ u✝ s1 s2 : Seq α
h : ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
s✝ t u : Seq α
x✝ : α
s : Seq α
⊢ ∃ s_1 t_1 u_1,
    append (append s t) u = append (append s_1 t_1) u_1 ∧ append s (append t u) = append s_1 (append t_1 u_1)
exact ⟨s, t, u, rfl, rfl⟩
no goals
case r
α : Type u
β : Type v
γ : Type w
s t u : Seq α
⊢ ∃ s_1 t_1 u_1,
    append (append s t) u = append (append s_1 t_1) u_1 ∧ append s (append t u) = append s_1 (append t_1 u_1)
exact ⟨s, t, u, rfl, rfl⟩