α : Type u
β : Type v
γ : Type w
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
⊢ IsBisimulation fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s
α : Type u
β : Type v
γ : Type w
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
⊢ f s = g s
refine' eq_of_bisim (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) _ ⟨s, rfl, rfl⟩
α : Type u
β : Type v
γ : Type w
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
s1 s2 : Seq β
h : ∃ s, s1 = f s ∧ s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct s1) (destruct s2)
α : Type u
β : Type v
γ : Type w
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
⊢ IsBisimulation fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s
intro s1 s2 h
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct s1) (destruct s2)
α : Type u
β : Type v
γ : Type w
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
s1 s2 : Seq β
h : ∃ s, s1 = f s ∧ s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct s1) (destruct s2)
rcases h with ⟨s, h1, h2⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct s1) (destruct s2)
rw [h1, h2]
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
s✝ : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (destruct (f s)) (destruct (g s))
apply H