Support for Inductive datatype with instance parameters

Nobody has claimed this yet.

There is a need to extend Lean4 to Smt translation to properly handle inductive data types with instance parameters. Examples:

```lean
inductive NatGroupParam (x : Nat) where
| first (n : Nat) (h1 : n ≥ x) (h2 : n < x + 100) : NatGroupParam x
| second (n : Nat) (h1 : n > x + 100) (h2 : n < x + 200) : NatGroupParam x
| next (n : NatGroupParam x)
```

```lean
structure Fin (n : Nat) where
/-- Creates a `Fin n` from `i : Nat` and a proof that `i < n`. -/
mk ::
/-- If `i : Fin n`, then `i.val : ℕ` is the described number. It can also be
written as `i.1` or just `i` when the target type is known. -/
val : Nat
/-- If `i : Fin n`, then `i.2` is a proof that `i.1 < n`. -/
isLt : LT.lt val n

```

---
**Transferred from:** input-output-hk/sc-fvt#246

Start by locating the Lean4-to-SMT translation entry point for inductive declarations and reproduce the two examples from the issue. Check how instance parameters are represented during translation; done means both NatGroupParam and Fin translate correctly without losing their parameters.

Written by the indexing model from the issue text.