Ssreflect Users Discussion List

[Vincent Siles <>]

Hello everybody,

I'm facing a quite annoying situation, and I think someone here might
already know a solution:

sometimes, I have to define function over non-trivial matrices (let's
say f: forall n, 'M[R]_n.+1 -> T).
When I try to prove properties about f by induction, the recursive
case usually unfold too much because
now my size is some n.+2 and the goal because unreadable.

In such cases, is there a known solution to "block" the unfolding ?

Best,
Vincent

PS: if necessary I can provide a small example