Ssreflect Users Discussion List

[Boris Djalal <>]

Hi Emilio,

You are right, it is in the manual (page 24), "rewrite h => -[]." does 
the job.

Thank you

On 03/09/2017 07:46 PM, Emilio Jesús Gallego Arias wrote:
> Dear Boris,
>
> Boris Djalal 
> <>
>  writes:
>
> > P, Q, R : Prop
> > h : P = Q
> > ============================
> > P /\ R -> R
> >
> > If I do "rewrite h => []", I obtain the following goal: Q /\ R -> R
> > whereas I expect to obtain: Q -> R -> R.
> You need to do "rewrite => -[]".
>
> If you look closely in the manual you will see that indeed "[]" as the
> first token after => is interpreted not as case, but as a "disjunctive
> introduction", as in "elim: n => [|n ihn]" .
>
> [Anyways I don't know all the details but indeed I do remember the
>   manual did a good job explaining this]
>
> --
> Emilio