Определение решаемого равенства для обобщенных индуктивных типов в agda

Ниже у меня есть ванильный индуктивный тип данных для некоторых формул, и мне интересно, есть ли способ оптимизировать этот процесс для определения решаемого равенства по любому индуктивно определенному типу внутри Agda (то есть без использования некоторых прагм или какой-либо другой функции метапрограммирования).

В частности, есть ли способ определить *ConstrInherets* конструктора любого типа любой арности. а затем использовать это параметрически для любого случая в решаемом определении равенства (поскольку мы должны сопоставить шаблон более with некоторое количество раз линейно по отношению к арности конструктора) и устранить весь no (λ ()) шум для конструкторов различных типов?

Кроме того, нарушается ли это при использовании более интересных индуктивных типов (параметризованных, индексированных, индуктивно-рекурсивных и т. Д.)?

Это похоже на пример определения, которое вполне естественно можно было бы определить в coq с помощью Ltac, и все же довольно болезненно и некрасиво в Agda, но если это не так, я был бы признателен за ссылки, где я мог бы прочитать об этом больше. .

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)

open import Data.Nat using (ℕ ; zero; suc ; _+_; _≟_)
open import Data.Empty

-- type symbols
data tSymb : Set where
  base : ℕ → tSymb
  ~ : tSymb → tSymb
  _\\_ : tSymb → tSymb → tSymb
  _//_ : tSymb → tSymb → tSymb

baseConstrInherets¬ : {x y : ℕ} → ¬ x ≡ y → ¬ base x ≡ base y
baseConstrInherets¬ ¬xy refl = ¬xy refl

~ConstrInherets¬ : {x y : tSymb} → ¬ x ≡ y → ¬ ~ x ≡ ~ y
~ConstrInherets¬ ¬xy refl = ¬xy refl

\\ConstrInherets¬L : {x y z1 z2 : tSymb} → ¬ x ≡ y → ¬ x \\ z1 ≡ y \\ z2
\\ConstrInherets¬L ¬xy refl = ¬xy refl

//ConstrInherets¬L : {x y z1 z2 : tSymb} → ¬ x ≡ y → ¬ x // z1 ≡ y // z2
//ConstrInherets¬L ¬xy refl = ¬xy refl

\\ConstrInherets¬R : {x y z : tSymb} → ¬ x ≡ y → ¬ z \\ x ≡ z \\ y
\\ConstrInherets¬R ¬xy refl = ¬xy refl

//ConstrInherets¬R : {x y z : tSymb} → ¬ x ≡ y → ¬ z // x ≡ z // y
//ConstrInherets¬R ¬xy refl = ¬xy refl

eql-tSymb : Decidable {A = tSymb} _≡_
eql-tSymb (base x) (base y) with Data.Nat._≟_ x y
... | no ¬p = false because (ofⁿ (baseConstrInherets¬ ¬p))
... | yes refl = true because ofʸ refl
eql-tSymb (base x) (~ y) = no (λ ())
eql-tSymb (base x) (y \\ y₁) = no (λ ())
eql-tSymb (base x) (y // y₁) = no (λ ())
eql-tSymb (~ x) (base x₁) = no (λ ())
eql-tSymb (~ x) (~ y) with eql-tSymb x y
... | no ¬p = false because (ofⁿ (~ConstrInherets¬ ¬p))
... | yes refl = true because (ofʸ refl)
eql-tSymb (~ x) (y \\ y₁) = no (λ ())
eql-tSymb (~ x) (y // y₁) = no (λ ())
eql-tSymb (x \\ x₁) (base x₂) = no (λ ())
eql-tSymb (x \\ x₁) (~ y) = no (λ ())
eql-tSymb (x \\ x₁) (y \\ y₁) with eql-tSymb x y
... | no ¬p          = false because (ofⁿ (\\ConstrInherets¬L ¬p))
... | yes refl with eql-tSymb x₁ y₁
... | no ¬p = false because (ofⁿ (\\ConstrInherets¬R ¬p))
... | yes refl = true because ofʸ refl
eql-tSymb (x \\ x₁) (y // y₁) = no (λ ())
eql-tSymb (x // x₁) (base x₂) = no (λ ())
eql-tSymb (x // x₁) (~ y) = no (λ ())
eql-tSymb (x // x₁) (y \\ y₁) = no (λ ())
eql-tSymb (x // x₁) (y // y₁) with eql-tSymb x y
... | no ¬p          = false because (ofⁿ (//ConstrInherets¬L ¬p))
... | yes refl with eql-tSymb x₁ y₁
... | no ¬p = false because (ofⁿ (//ConstrInherets¬R ¬p))
... | yes refl = true because ofʸ refl

Примечание. Это следующий вопрос к Как определить подформулу индуктивно определенного типа в Agda?