refactor(FirstOrder): ClosedSemiterm, Closedterm (#519)

Author: iehality

Foundation/FirstOrder/Arithmetic/Basic/ORingStruc.lean

@@ -149,7 +149,7 @@ end
 
 open Semiterm Semiformula
 
-abbrev Polynomial (n : ℕ) : Type := Semiterm ℒₒᵣ Empty n
+abbrev Polynomial (n : ℕ) : Type := ClosedSemiterm ℒₒᵣ n
 
 class Structure.ORing (L : Language) [L.ORing] (M : Type w) [ORingStruc M] [Structure L M] extends
   Structure.Zero L M, Structure.One L M, Structure.Add L M, Structure.Mul L M, Structure.Eq L M, Structure.LT L M

Foundation/FirstOrder/Basic/Coding.lean

@@ -61,7 +61,7 @@ lemma encode_eq_toNat (t : Semiterm L ξ n) : encode t = toNat t := rfl
 lemma toNat_func {k} (f : L.Func k) (v : Fin k → Semiterm L ξ n) :
     toNat (func f v) = (Nat.pair 2 <| Nat.pair k <| Nat.pair (encode f) <| Matrix.vecToNat fun i ↦ toNat (v i)) + 1 := rfl
 
-@[simp] lemma encode_emb (t : Semiterm L Empty n) : encode (Rew.emb t : Semiterm L ξ n) = encode t := by
+@[simp] lemma encode_emb (t : ClosedSemiterm L n) : encode (Rew.emb t : Semiterm L ξ n) = encode t := by
   simp only [encode_eq_toNat]
   induction t
   · simp [toNat]

Foundation/FirstOrder/Basic/Operator.lean

@@ -10,15 +10,15 @@ variable {L : Language}
 namespace Semiterm
 
 structure Operator (L : Language) (n : ℕ) where
-  term : Semiterm L Empty n
+  term : ClosedSemiterm L n
 
 abbrev Const (L : Language.{u}) := Operator L 0
 
 def fn {k} (f : L.Func k) : Operator L k := ⟨Semiterm.func f (#·)⟩
 
 namespace Operator
 
-def equiv : Operator L n ≃ Semiterm L Empty n where
+def equiv : Operator L n ≃ ClosedSemiterm L n where
   toFun := Operator.term
   invFun := Operator.mk
   left_inv := by intro _; simp

Foundation/FirstOrder/Basic/Semantics/Semantics.lean

@@ -75,11 +75,11 @@ def val (s : Structure L M) (e : Fin n → M) (ε : ξ → M) : Semiterm L ξ n
   | &x       => ε x
   | func f v => s.func f (fun i => (v i).val s e ε)
 
-abbrev valb (s : Structure L M) (e : Fin n → M) (t : Semiterm L Empty n) : M := t.val s e Empty.elim
+abbrev valb (s : Structure L M) (e : Fin n → M) (t : ClosedSemiterm L n) : M := t.val s e Empty.elim
 
 abbrev valm (M : Type w) [s : Structure L M] {n} (e : Fin n → M) (ε : ξ → M) : Semiterm L ξ n → M := val s e ε
 
-abbrev valbm (M : Type w) [s : Structure L M] {n} (e : Fin n → M) : Semiterm L Empty n → M := valb s e
+abbrev valbm (M : Type w) [s : Structure L M] {n} (e : Fin n → M) : ClosedSemiterm L n → M := valb s e
 
 abbrev realize (s : Structure L M) (t : Term L M) : M := t.val s ![] id
 
@@ -141,7 +141,7 @@ lemma val_embSubsts (w : Fin k → Semiterm L ξ n) (t : Semiterm L Empty k) :
     valb s e (Rew.toS t) = val s ![] e t := by
   simp [val_rew, Matrix.empty_eq]; congr
 
-@[simp] lemma val_toF {e : Fin n → M} (t : Semiterm L Empty n) :
+@[simp] lemma val_toF {e : Fin n → M} (t : ClosedSemiterm L n) :
     val s ![] e (Rew.toF t) = valb s e t := by
   simp only [val_rew]; congr; funext i; contradiction
 
@@ -151,7 +151,7 @@ variable (φ : L₁ →ᵥ L₂) (e : Fin n → M) (ε : ξ → M)
 
 lemma val_lMap (φ : L₁ →ᵥ L₂) (s₂ : Structure L₂ M) (e : Fin n → M) (ε : ξ → M) {t : Semiterm L₁ ξ n} :
     (t.lMap φ).val s₂ e ε = t.val (s₂.lMap φ) e ε :=
-  by induction t <;> simp [*, valm, Function.comp_def, val_func, Semiterm.lMap_func]
+  by induction t <;> simp [*, val_func, Semiterm.lMap_func]
 
 end Language
 
@@ -231,7 +231,7 @@ def EvalAux (s : Structure L M) (ε : ξ → M) : ∀ {n}, (Fin n → M) → Sem
 
 @[simp] lemma EvalAux_neg (φ : Semiformula L ξ n) :
     EvalAux s ε e (∼φ) = ¬EvalAux s ε e φ :=
-  by induction φ using rec' <;> simp [*, EvalAux, ←neg_eq, or_iff_not_imp_left]
+  by induction φ using rec' <;> simp [*, EvalAux, or_iff_not_imp_left]
 
 def Eval (s : Structure L M) (e : Fin n → M) (ε : ξ → M) : Semiformula L ξ n →ˡᶜ Prop where
   toTr := EvalAux s ε e
@@ -240,7 +240,7 @@ def Eval (s : Structure L M) (e : Fin n → M) (ε : ξ → M) : Semiformula L 
   map_and' := by simp [EvalAux]
   map_or' := by simp [EvalAux]
   map_neg' := by simp [EvalAux_neg]
-  map_imply' := by simp [imp_eq, EvalAux_neg, ←neg_eq, EvalAux, imp_iff_not_or]
+  map_imply' := by simp [EvalAux_neg, ←neg_eq, EvalAux, imp_iff_not_or]
 
 abbrev Evalm (M : Type w) [s : Structure L M] {n} (e : Fin n → M) (ε : ξ → M) :
     Semiformula L ξ n →ˡᶜ Prop := Eval s e ε
@@ -647,7 +647,7 @@ noncomputable instance nonemptyModelOfSat (h : Semantics.Satisfiable (Struc.{v,
   choose i _ _ using Classical.choose_spec (satisfiable_iff.mp h); exact i
 
 noncomputable def StructureModelOfSatAux (h : Semantics.Satisfiable (Struc.{v, u} L) T) :
-    { s : Structure L (ModelOfSat h) // ModelOfSat h ⊧ₘ* T } := by
+    { _s : Structure L (ModelOfSat h) // ModelOfSat h ⊧ₘ* T } := by
   choose _ s h using Classical.choose_spec (satisfiable_iff.mp h)
   exact ⟨s, h⟩
 
@@ -729,7 +729,7 @@ variable {M : Type u} [Nonempty M] [s₂ : Structure L₂ M]
 
 lemma modelsTheory_onTheory₁ {T₁ : Theory L₁} :
     ModelsTheory (s := s₂) M (T₁.lMap Φ) ↔ ModelsTheory (s := s₂.lMap Φ) M T₁ :=
-  by simp [Semiformula.models_lMap, Theory.lMap, modelsTheory_iff, @modelsTheory_iff (T := T₁)]
+  by simp [Semiformula.models_lMap, Theory.lMap, @modelsTheory_iff (T := T₁)]
 
 end Theory
 

Foundation/FirstOrder/Basic/Syntax/Rew.lean

@@ -236,11 +236,11 @@ lemma coe_rel [IsEmpty ο] {k : ℕ} (R : L.Rel k) (v : Fin k → Semiterm L ο
 lemma coe_nrel [IsEmpty ο] {k : ℕ} (R : L.Rel k) (v : Fin k → Semiterm L ο n) :
     (Rewriting.embedding (nrel R v) : Semiformula L ξ n) = (nrel R fun i ↦ Rew.emb (v i)) := by rfl
 
-lemma coe_substitute_eq_substitute_coe (φ : Semisentence L k) (v : Fin k → Semiterm L Empty n) :
+lemma coe_substitute_eq_substitute_coe (φ : Semisentence L k) (v : Fin k → ClosedSemiterm L n) :
     (↑(φ ⇜ v) : SyntacticSemiformula L n) = (↑φ : SyntacticSemiformula L k)⇜(fun i ↦ (↑(v i) : Semiterm L ℕ n)) :=
   Rewriting.embedding_substitute_eq_substitute_embedding φ v
 
-lemma coe_substs_eq_substs_coe₁ (φ : Semisentence L 1) (t : Semiterm L Empty n) :
+lemma coe_substs_eq_substs_coe₁ (φ : Semisentence L 1) (t : ClosedSemiterm L n) :
     (↑(φ/[t]) : SyntacticSemiformula L n) = (↑φ : SyntacticSemiformula L 1)/[(↑t : Semiterm L ℕ n)] :=
   Rewriting.embedding_substs_eq_substs_coe₁ φ t
 

Foundation/FirstOrder/Internal/DerivabilityCondition/D3.lean

@@ -36,7 +36,7 @@ noncomputable abbrev toNumVec (w : Fin n → V) : SemitermVec V ℒₒᵣ n k :=
 
 variable (T)
 
-theorem term_complete {n : ℕ} (t : FirstOrder.Semiterm ℒₒᵣ Empty n) (w : Fin n → V) :
+theorem term_complete {n : ℕ} (t : FirstOrder.ClosedSemiterm ℒₒᵣ n) (w : Fin n → V) :
     T.internalize V ⊢! (toNumVec w ⤕ ⌜t⌝) ≐  𝕹 (t.valbm V w) :=
   match t with
   |                         #z => by simp

Foundation/FirstOrder/Internal/Syntax/Formula/Coding.lean

@@ -249,16 +249,16 @@ noncomputable instance : LCWQIsoGoedelQuote (Semisentence L) (Metamath.Semiformu
 def empty_typed_quote_def (σ : Semisentence L n) :
     (⌜σ⌝ : Metamath.Semiformula V L n) = ⌜(Rewriting.embedding σ : SyntacticSemiformula L n)⌝ := rfl
 
-@[simp] lemma empty_typed_quote_eq (t u : Semiterm ℒₒᵣ Empty n) :
+@[simp] lemma empty_typed_quote_eq (t u : ClosedSemiterm ℒₒᵣ n) :
     (⌜(“!!t = !!u” : Semisentence ℒₒᵣ n)⌝ : Metamath.Semiformula V ℒₒᵣ n) = (⌜t⌝ ≐ ⌜u⌝) := rfl
 
-@[simp] lemma empty_typed_quote_ne (t u : Semiterm ℒₒᵣ Empty n) :
+@[simp] lemma empty_typed_quote_ne (t u : ClosedSemiterm ℒₒᵣ n) :
     (⌜(“!!t ≠ !!u” : Semisentence ℒₒᵣ n)⌝ : Metamath.Semiformula V ℒₒᵣ n) = (⌜t⌝ ≉ ⌜u⌝) := rfl
 
-@[simp] lemma empty_typed_quote_lt (t u : Semiterm ℒₒᵣ Empty n) :
+@[simp] lemma empty_typed_quote_lt (t u : ClosedSemiterm ℒₒᵣ n) :
     (⌜(“!!t < !!u” : Semisentence ℒₒᵣ n)⌝ : Metamath.Semiformula V ℒₒᵣ n) = (⌜t⌝ <' ⌜u⌝) := rfl
 
-@[simp] lemma empty_typed_quote_nlt (t u : Semiterm ℒₒᵣ Empty n) :
+@[simp] lemma empty_typed_quote_nlt (t u : ClosedSemiterm ℒₒᵣ n) :
     (⌜(“!!t ≮ !!u” : Semisentence ℒₒᵣ n)⌝ : Metamath.Semiformula V ℒₒᵣ n) = (⌜t⌝ ≮' ⌜u⌝) := rfl
 
 noncomputable instance : GoedelQuote (Semisentence L n) V where

Foundation/FirstOrder/Internal/Syntax/Term/Coding.lean

@@ -147,43 +147,43 @@ lemma coe_quote_eq_quote' (t : SyntacticSemiterm L n) :
 
 variable (V)
 
-noncomputable instance : GoedelQuote (Semiterm L Empty n) (Metamath.Semiterm V L n) where
+noncomputable instance : GoedelQuote (ClosedSemiterm L n) (Metamath.Semiterm V L n) where
   quote t := ⌜(Rew.emb t : SyntacticSemiterm L n)⌝
 
 variable {V}
 
-def empty_typed_quote_def (t : Semiterm L Empty n) :
+def empty_typed_quote_def (t : ClosedSemiterm L n) :
     (⌜t⌝ : Metamath.Semiterm V L n) = ⌜(Rew.emb t : SyntacticSemiterm L n)⌝ := rfl
 
 @[simp] lemma empty_typed_quote_bvar (x : Fin n) :
-    (⌜(#x : Semiterm L Empty n)⌝ : Metamath.Semiterm V L n) = Metamath.Semiterm.bvar x := rfl
+    (⌜(#x : ClosedSemiterm L n)⌝ : Metamath.Semiterm V L n) = Metamath.Semiterm.bvar x := rfl
 
-@[simp] lemma empty_typed_quote_func (f : L.Func k) (v : Fin k → Semiterm L Empty n) :
+@[simp] lemma empty_typed_quote_func (f : L.Func k) (v : Fin k → ClosedSemiterm L n) :
     (⌜func f v⌝ : Metamath.Semiterm V L n) = Metamath.Semiterm.func f fun i ↦ ⌜v i⌝ := rfl
 
-@[simp] lemma empty_typed_quote_add (t u : Semiterm ℒₒᵣ Empty n) :
-    (⌜(‘!!t + !!u’ : Semiterm ℒₒᵣ Empty n)⌝ : Metamath.Semiterm V ℒₒᵣ n) = ⌜t⌝ + ⌜u⌝ := rfl
+@[simp] lemma empty_typed_quote_add (t u : ClosedSemiterm ℒₒᵣ n) :
+    (⌜(‘!!t + !!u’ : ClosedSemiterm ℒₒᵣ n)⌝ : Metamath.Semiterm V ℒₒᵣ n) = ⌜t⌝ + ⌜u⌝ := rfl
 
-@[simp] lemma empty_typed_quote_mul (t u : Semiterm ℒₒᵣ Empty n) :
-    (⌜(‘!!t * !!u’ : Semiterm ℒₒᵣ Empty n)⌝ : Metamath.Semiterm V ℒₒᵣ n) = ⌜t⌝ * ⌜u⌝ := rfl
+@[simp] lemma empty_typed_quote_mul (t u : ClosedSemiterm ℒₒᵣ n) :
+    (⌜(‘!!t * !!u’ : ClosedSemiterm ℒₒᵣ n)⌝ : Metamath.Semiterm V ℒₒᵣ n) = ⌜t⌝ * ⌜u⌝ := rfl
 
 @[simp] lemma empty_typed_quote_numeral_eq_numeral (k : ℕ) :
-    (⌜(↑k : Semiterm ℒₒᵣ Empty n)⌝ : Metamath.Semiterm V ℒₒᵣ n) = typedNumeral ↑k := by
+    (⌜(↑k : ClosedSemiterm ℒₒᵣ n)⌝ : Metamath.Semiterm V ℒₒᵣ n) = typedNumeral ↑k := by
   simp [empty_typed_quote_def]
 
-noncomputable instance : GoedelQuote (Semiterm L Empty n) V where
+noncomputable instance : GoedelQuote (ClosedSemiterm L n) V where
   quote t := ⌜(Rew.emb t : SyntacticSemiterm L n)⌝
 
-lemma empty_quote_def (t : Semiterm L Empty n) : (⌜t⌝ : V) = ⌜(Rew.emb t : SyntacticSemiterm L n)⌝ := rfl
+lemma empty_quote_def (t : ClosedSemiterm L n) : (⌜t⌝ : V) = ⌜(Rew.emb t : SyntacticSemiterm L n)⌝ := rfl
 
-def empty_quote_eq (t : Semiterm L Empty n) : (⌜t⌝ : V) = (⌜t⌝ : Metamath.Semiterm V L n).val := rfl
+def empty_quote_eq (t : ClosedSemiterm L n) : (⌜t⌝ : V) = (⌜t⌝ : Metamath.Semiterm V L n).val := rfl
 
-lemma empty_quote_eq_encode (t : Semiterm L Empty n) : (⌜t⌝ : V) = ↑(encode t) := by simp [empty_quote_def, quote_eq_encode]
+lemma empty_quote_eq_encode (t : ClosedSemiterm L n) : (⌜t⌝ : V) = ↑(encode t) := by simp [empty_quote_def, quote_eq_encode]
 
 @[simp] lemma coe_quote {ξ n} (t : SyntacticSemiterm L n) : ↑(⌜t⌝ : ℕ) = (⌜t⌝ : Semiterm ℒₒᵣ ξ m) := by
   simp [goedelNumber'_def, quote_eq_encode]
 
-@[simp] lemma coe_empty_quote {ξ n} (t : Semiterm L Empty n) : ↑(⌜t⌝ : ℕ) = (⌜t⌝ : Semiterm ℒₒᵣ ξ m) := by
+@[simp] lemma coe_empty_quote {ξ n} (t : ClosedSemiterm L n) : ↑(⌜t⌝ : ℕ) = (⌜t⌝ : Semiterm ℒₒᵣ ξ m) := by
   simp [goedelNumber'_def, empty_quote_eq_encode]
 
 end LO.FirstOrder.Semiterm

Foundation/Logic/LogicSymbol.lean

@@ -145,7 +145,8 @@ variable {α β γ}
 
 instance : FunLike (α →ˡᶜ β) α β where
   coe := toTr
-  coe_injective' := by intro f g h; rcases f; rcases g; simp; exact h
+  coe_injective' := by
+    intro f g h; rcases f; rcases g; simpa using h
 
 instance : CoeFun (α →ˡᶜ β) (fun _ => α → β) := DFunLike.hasCoeToFun
 
@@ -244,15 +245,16 @@ def conjLt (φ : ℕ → α) : ℕ → α
 
 @[simp] lemma hom_conj_prop [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (φ : ℕ → α) :
     f (conjLt φ k) ↔ ∀ i < k, f (φ i) := by
-  induction' k with k ih <;> simp [*]
-  constructor
-  · rintro ⟨hk, h⟩
-    intro i hi
-    rcases Nat.eq_or_lt_of_le (Nat.le_of_lt_succ hi) with (rfl | hi)
-    · exact hk
-    · exact h i hi
-  · rintro h
-    exact ⟨h k (by simp), fun i hi ↦ h i (Nat.lt_add_right 1 hi)⟩
+  induction' k with k ih
+  · simp [*]
+  · suffices (f (φ k) ∧ ∀ i < k, f (φ i)) ↔ ∀ i < k + 1, f (φ i) by simp [*]
+    constructor
+    · rintro ⟨hk, h⟩
+      intro i hi
+      rcases Nat.eq_or_lt_of_le (Nat.le_of_lt_succ hi) with (rfl | hi)
+      · exact hk
+      · exact h i hi
+    · grind
 
 def disjLt (φ : ℕ → α) : ℕ → α
   | 0     => ⊥
@@ -264,15 +266,10 @@ def disjLt (φ : ℕ → α) : ℕ → α
 
 @[simp] lemma hom_disj_prop [FunLike F α Prop] [LogicalConnective.HomClass F α Prop] (f : F) (φ : ℕ → α) :
     f (disjLt φ k) ↔ ∃ i < k, f (φ i) := by
-  induction' k with k ih <;> simp [*]
-  constructor
-  · rintro (h | ⟨i, hi, h⟩)
-    · exact ⟨k, by simp, h⟩
-    · exact ⟨i, Nat.lt_add_right 1 hi, h⟩
-  · rintro ⟨i, hi, h⟩
-    rcases Nat.eq_or_lt_of_le (Nat.le_of_lt_succ hi) with (rfl | hi)
-    · left; exact h
-    · right; exact ⟨i, hi, h⟩
+  induction' k with k ih
+  · simp [*]
+  · suffices (f (φ k) ∨ ∃ i < k, f (φ i)) ↔ ∃ i < k + 1, f (φ i) by simp [*]
+    grind
 
 end conjdisj
 
@@ -316,15 +313,19 @@ variable [LogicalConnective α] [LogicalConnective β]
 
 @[simp] lemma conj_hom_prop [FunLike F α Prop] [LogicalConnective.HomClass F α Prop]
   (f : F) (v : Fin n → α) : f (conj v) = ∀ i, f (v i) := by
-  induction' n with n ih <;> simp [conj]
-  · simp [ih]; constructor
+  induction' n with n ih
+  · simp [conj]
+  · suffices (f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)) ↔ ∀ (i : Fin (n + 1)), f (v i) by simpa [conj, ih]
+    constructor
     · intro ⟨hz, hs⟩ i; cases i using Fin.cases; { exact hz }; { exact hs _ }
     · intro h; exact ⟨h 0, fun i => h _⟩
 
 @[simp] lemma disj_hom_prop [FunLike F α Prop] [LogicalConnective.HomClass F α Prop]
   (f : F) (v : Fin n → α) : f (disj v) = ∃ i, f (v i) := by
-  induction' n with n ih <;> simp [disj]
-  · simp [ih]; constructor
+  induction' n with n ih
+  · simp [disj]
+  · suffices (f (v 0) ∨ ∃ i, f (vecTail v i)) ↔ ∃ i, f (v i) by simpa [disj, ih]
+    constructor
     · rintro (H | ⟨i, H⟩); { exact ⟨0, H⟩ }; { exact ⟨i.succ, H⟩ }
     · rintro ⟨i, h⟩
       cases i using Fin.cases; { left; exact h }; { right; exact ⟨_, h⟩ }
@@ -600,16 +601,8 @@ variable [LogicalConnective α]
 
 lemma map_conj_union [DecidableEq α] [FunLike F α Prop] [LogicalConnective.HomClass F α Prop]
     (f : F) (s₁ s₂ : Finset α) : f (s₁ ∪ s₂).conj ↔ f (s₁.conj ⋏ s₂.conj) := by
-  simp
-  constructor;
-  . intro h;
-    constructor;
-    . intro a ha;
-      exact h a (Or.inl ha);
-    . intro a ha;
-      exact h a (Or.inr ha);
-  . intro ⟨h₁, h₂⟩ a ha;
-    cases ha <;> simp_all;
+  suffices (∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a) ↔ (∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a by simpa
+  grind
 
 lemma map_conj' {β : Type*} [LogicalConnective β] [FunLike F α β] [LogicalConnective.HomClass F α β]
     (Φ : F) (s : Finset ι) (f : ι → α) : Φ (⩕ i ∈ s, f i) = ⩕ i ∈ s, Φ (f i) := by
@@ -630,14 +623,8 @@ lemma map_uconj [LogicalConnective β] [FunLike F α β] [LogicalConnective.HomC
 
 lemma map_disj_union [DecidableEq α] [FunLike F α Prop] [LogicalConnective.HomClass F α Prop]
     (f : F) (s₁ s₂ : Finset α) : f (s₁ ∪ s₂).disj ↔ f (s₁.disj ⋎ s₂.disj) := by
-  simp [map_disj_prop];
-  constructor;
-  . rintro ⟨a, h₁ | h₂, hb⟩;
-    . left; use a;
-    . right; use a;
-  . rintro (⟨a₁, h₁⟩ | ⟨a₂, h₂⟩);
-    . use a₁; simp_all;
-    . use a₂; simp_all;
+  suffices (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) ↔ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a by simpa [map_disj_prop]
+  grind
 
 lemma map_disj' [LogicalConnective β] [FunLike F α β] [LogicalConnective.HomClass F α β]
     (Φ : F) (s : Finset ι) (f : ι → α) : Φ (⩖ i ∈ s, f i) = ⩖ i ∈ s, Φ (f i) := by

Foundation/Logic/Predicate/Language.lean

@@ -120,11 +120,13 @@ instance (k) : ToString (oRing.Rel k) :=
   | Rel.eq => "\\mathrm{Eq}"
   | Rel.lt    => "\\mathrm{LT}"⟩
 
-instance (k) : DecidableEq (oRing.Func k) := fun a b =>
-  by rcases a <;> rcases b <;> simp <;> try {exact instDecidableTrue} <;> try {exact instDecidableFalse}
+instance (k) : DecidableEq (oRing.Func k) := fun a b => by
+  rcases a <;> rcases b <;>
+  simp only [reduceCtorEq] <;> try {exact instDecidableTrue} <;> try {exact instDecidableFalse}
 
-instance (k) : DecidableEq (oRing.Rel k) := fun a b =>
-  by rcases a <;> rcases b <;> simp <;> try {exact instDecidableTrue} <;> try {exact instDecidableFalse}
+instance (k) : DecidableEq (oRing.Rel k) := fun a b => by
+  rcases a <;> rcases b <;>
+  simp only [reduceCtorEq] <;> try {exact instDecidableTrue} <;> try {exact instDecidableFalse}
 
 instance (k) : Encodable (oRing.Func k) where
   encode := fun x =>