simp [Rew.rel, Rew.nrel, *]
case hex
L : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
n : ?m.1833779
n₁ n₂ n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
a✝ : ∀ (ω : Rew L ξ₁ (n✝ + 1) ξ₂ n₂), (ω.hom p✝).Open ↔ p✝.Open
ω : Rew L ξ₁ n✝ ξ₂ n₂
⊢ (ω.hom (∃' p✝)).Open ↔ (∃' p✝).Open
no goals