intro e
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₂ : ℕ
ω : Rew L Empty n₁ Empty n₂
a✝¹ : HSemiformula L Empty n₁ (𝚺, m)
a✝ : HSemiformula L Empty n₁ (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
⊢ ∀ (e : Fin n₂ → M),
    (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝¹.val ↔
      (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝.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₂ : ℕ
ω : Rew L Empty n₁ Empty n₂
a✝¹ : HSemiformula L Empty n₁ (𝚺, m)
a✝ : HSemiformula L Empty n₁ (𝚷, m)
h : ProperOn M (a✝¹.mkDelta a✝)
e : Fin n₂ → M
⊢ (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝¹.val ↔
    (Semiformula.Eval inst✝¹ (fun x => Semiterm.val inst✝¹ e Empty.elim (ω #x)) Empty.elim) a✝.val