simp [ProperOn, HSemiformula.rew, Semiformula.eval_rew, Function.comp, h.iff, Empty.eq_elim]
case mkDelta
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
f : Fin n₁ → Semiterm L M n₂
a✝¹ : HSemiformula L M n₁ (𝚺, m)
a✝ : HSemiformula L M n₁ (𝚷, m)
h : ProperWithParamOn M (a✝¹.mkDelta a✝)
e : Fin n₂ → M
⊢ (Semiformula.Evalm M e id) (HSemiformula.rew (Rew.substs f) (a✝¹.mkDelta a✝)).sigma.val ↔
    (Semiformula.Evalm M e id) (HSemiformula.rew (Rew.substs f) (a✝¹.mkDelta a✝)).pi.val
case mkDelta
L : Language
inst✝⁷ : L.ORing
ξ : Type v
n : ℕ
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : Structure L M
inst✝ : Structure.ORing L M
n₁ m n₂ : ℕ
f : Fin n₁ → Semiterm L M n₂
a✝¹ : HSemiformula L M n₁ (𝚺, m)
a✝ : HSemiformula L M n₁ (𝚷, m)
h : ProperWithParamOn M (a✝¹.mkDelta a✝)
e : Fin n₂ → M
⊢ (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e id (f x)) fun x => x) a✝¹.val ↔
    (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e id (f x)) fun x => x) a✝.val