Bug: smt translation error for mutually recursive funtions with different params

Translation or index out of bounds error is triggered when translating mutually recursive functions with different number of parameters. E.g.

```
inductive Data where
| Constr : Int → List Data → Data
| List : List Data → Data
| I : Int → Data
| B : String → Data

mutual
def eqData : Data → Data → Bool
| .Constr i args, .Constr i' args' => eqDataConstr i args i' args'
| .List l, .List l' => eqDataList l l'
| .I i, .I i' => i == i'
| .B b, .B b' => b == b'
| _ , _ => false

def eqDataList : List Data → List Data → Bool
| [] , [] => true
| x :: xs, y :: ys => eqData x y && eqDataList xs ys
| _ , _ => false

def eqDataConstr : Int → List Data → Int → List Data → Bool
| i , args , i' , args' => (i == i') && eqDataList args args'
end

example : ∀ (i j : Nat) (xs ys : List Data), eqData (.Constr i xs) (.Constr (Int.ofNat j) [.List ys]) := by blaster (timeout: 5)
```