[Totalize pass] mishandling of partial functions calls inside partial functions

[DCupello1]

The following spec:

def $inv_isize(nat) : Inn hint(partial)
def $inv_jsize(nat) : Jnn hint(partial)

def $inv_isize(32) = I32
def $inv_isize(64) = I64
def $inv_jsize(8)  = I8
def $inv_jsize(16) = I16
def $inv_jsize(n)  = $inv_isize(n)

gets parsed and transformed into:

def $inv_jsize(nat : nat) : Jnn?
  def $inv_jsize(8) = ?(I8_Jnn)
  def $inv_jsize(16) = ?(I16_Jnn)
  def $inv_jsize{n : n}(n) = ?((!($inv_isize(n)) : Inn <: Jnn))
  def $inv_jsize{x0 : nat}(x0) = ?()

Which has two problems (say we input 3):

• the ?(!($inv_isize(3)) : Inn <: Jnn) would then be ?(!(None)) which unsure what would be the semantics of this
• It has the additional case def $inv_jsize{x0 : nat}(x0) = ?(), which specifically in Rocq it does not allow redundant clauses

This is an issue with the totalize pass since it applies the TheE to any partial function which doesn't particularly make sense here.