Hello,

I came across another problem with a similar expression type, as in my last question. I would like to prove decidable equality for this expression type.

```
Inductive Expression : Type :=
| EEmptyList
| ETuple (l : list Expression)
| EMap (l : list (Expression * Expression)).
Theorem expr_eq_dec : forall e e' : Expression, {e = e'} + {e <> e'}.
```

At first, the `EMap`

constructor had two lists instead of the product, and I managed to prove the property in question with `Fixpoint`

(like in this question), however, when using product inside the list, I get ill-formed recursion errors. I also tried to use the mentioned code about trees and json in the above mentioned thread, but I wasn’t able to formalise it in the case of `EMap`

-s (in this case both elements of the product are recursive, unlike in json code).

Is there an easy approach to generate or prove decidable equality for multiply nested inductive types or can I use somehow `Program Fixpoint`

here? Also is there a way to generate correct induction principles for types like this?