frenetic-lang/netkat — pull request #1 by seliopou (2013-10-16 01:34:01+00:00)
Title: bvector_eqdec: found a better way

The two major cases in bvector_eqdec reduce to cases in which the heads
of bvectors are not equal, or the tails of bvectors are not equal.
Separate those into two different lemmas, and write bvector_eqdec in
terms of those.