Error: «Introduced symbol cannot be removed.» Feature proposal job: primitive structure/record types to pack multiple arguments

Test problem:

constant symbol Set : TYPE;
injective symbol τ : Set → TYPE; builtin "T" ≔ τ;

symbol mys : TYPE;
symbol myop :  mys →  mys →   mys;

symbol testfun : Π (Func : Set) (Hom : τ Func → Set) (Comp : Π [F : τ Func]  , τ (Hom F)) ,
 mys;

// RULE ERROR: "Introduced symbol [$179144] cannot be removed."
rule (myop (@testfun $Func $Hom $Comp ) (@testfun $Func $Hom $Comp    ) )
    ↪  (@testfun $Func $Hom $Comp ) ;

Could anyone clarify what this error means? Temporary solution: this is solved by packing all the arguments of testfun into one value of a new inductive record/structure type.
Any future plans for an implementation of automatic/better support of structure/records with (primitive) projections in Lambdapi ?
Could the Lambdapi unif_rule command be used to simulate type classes or canonical structures, for (very) large library developments?
Here is the context: I have a Lambdapi implementation of Dosen's categorial logic/programming/proof-assistant with "abstract" automatic decidability of equality/convertibility, where "abstract" means that it is in reality a proof-assistant for proving categorial lemmas.

https://github.com/1337777/cartier/blob/master/cartierSolution13.lp

Now the next step is to link the "abstract" implementation to a "concrete" implementation of categorial datatype structures for concrete computations, everything still within Lambdapi.

And Lambdapi is currently the only framework, because of logical-dependent types and computational-rewrite rules, capable of merging both the "abstract" implementation for computationally-proving with the "concrete" implementation for computing, with categories... For example,

https://explore.jobs.ufl.edu/en-us/job/527710/systems-adminprogrammer-iv

in this AlgebraicJulia, for a "type-safe concrete" implementation, they have to hack a pseudo-dependent-type domain-specific-language embedded within Julia...

Proposal: Lambdapi could employ somebody (or me) this 1 month of August to engineer tooling support for typeclasses or canonical-structures in Lambdapi.. and thereafter to produce a "concrete" (applied) implementation of categories which is linked to the existing "abstract" (prover) implementation. And I repeat that Lambdapi is currently in a unique strategic position to unify both worlds with a limitless payoff, n.b. that some entities linked above are already investing $100,000 - $130,000 (in a limited approach) ...

Voilà, à vous! Christopher

Deducteam / lambdapi

Error: «Introduced symbol cannot be removed.» Feature proposal job: primitive structure/record types to pack multiple arguments #1006