Handling of Type Class and Structure properties

Here is a need to properly handle type class and structure properties when translating to SMTLIB.
Indeed, we need to generate the proper assertions for type class instances, type class constraints as well as structure instances.
For instance, we should be able to automatically generate the necessary assertions for the given type class:
```lean
class Eq (α : Type) where
eq : α -> α -> Bool

/-- Properties on equality that need to be proved for each Eq instance. -/
eq_reflexive : ∀ (x : α), eq x x
eq_symmetric : ∀ (x y : α), eq x y → eq y x
eq_transitive : ∀ (x y z : α), eq x y → eq y z → eq x z
eq_commute : ∀ (x y : α), eq x y = eq y x
eq_equiv_struct_eq : ∀ (x y : α), eq x y → x = y
```

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

Start by locating the translation path from Lean type classes and structures to SMTLIB. Define the required assertions for type class instances, type class constraints, and structure instances, using the Eq example as a reference; done means these properties are generated automatically.

Written by the indexing model from the issue text.