Hi Everyone,

I’m currently working to prove results on a fonction `is_valid : A -> bool`

of the form `is_valid a = true -> % some property`

, where `A`

is an inductive type of the form

```
Inductive A := | N : B -> (list A) -> A . % N is the only constructor
```

And `B`

is also an inductive type **with around 50 constructors**.

The problem is that, in the `is_valid`

function, I have nested pattern matching (on the list) like

```
| N b1 (N b2 [])::(N b3 [])::_ -> (f b1 b2 b3) % some property computed using b1 b2 b3
```

generates huge patterns, because the internal translation of nested patterns is to create several levels of patterns. As my type `B`

has 50 constructors, each level of pattern matching generates **a lot** of subgoals and slows down the proofs.

Is there a simple way to say that if `is_valid a = true`

then all the possible cases are only the ones of the main pattern matching, without having to break all sub-levels of matching using `congruence`

everywhere ? Just doing an `unfold`

of the `is_valid`

function takes ~2 min on my computer. The dream would be that `is_valid a = true -> P`

could be split into the few subgoals of the form `(f b1 b2 b3) -> P`

Thank you for your help !

Clément

PS: I could write a big theorem saying that, but I’m looking for an automated way of doing it