simp
n✝ : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁ : Fin n✝ → M₁
ε₁✝ : μ → M₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
⊢ (Evalf s₂ (⇑φ ∘ ε₁)) (∀* p) → (Evalf s₁ ε₁) (∀* p)
n✝ : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁ : Fin n✝ → M₁
ε₁✝ : μ → M₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
⊢ (∀ (e : Fin n → M₂), (Eval s₂ e (⇑φ ∘ ε₁)) p) → ∀ (e : Fin n → M₁), (Eval s₁ e ε₁) p