Ssreflect Users Discussion List

[Filou Vincent <>]

Hi all,

I'm stuck in a proof at the following subgoal:
[set u \in V_of G | ((u, v) \in E_of G) || ((v, u) \in E_of G)] == [set 
u \in V_of G' | ((u, v') \in E_of G') || ((v', u) \in E_of G')]

Is there a way to transform it to something like

forall u, u \in V_of G ->(((u, v) \in E_of G) || ((v, u) \in E_of G)) == 
(((u, v') \in E_of G') || ((v', u) \in E_of G'))

?

And by the way, where can I find some documentation about the ssreflect 
library?

Thanks,
Vincent