Clean-up Vbase.v
There are a lot of definitions in Vbase.v that become redundant when we add ssreflect. We only need to define the tactics.
There are a lot of definitions in Vbase.v that become redundant when we add ssreflect. We only need to define the tactics.