Theorem: LO.FirstOrder.Rew.open_iff (Logic/FirstOrder/Basic/Syntax/Rew.lean)

State before:
L : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
n : ?m.1833779
n₁ n₂ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
⊢ (ω.hom p).Open ↔ p.Open
Tactic:
induction p using Semiformula.rec' <;> try simp [Rew.rel, Rew.nrel, *]
State after:
no goals

State before:
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
Tactic:
simp [Rew.rel, Rew.nrel, *]
State after:
no goals