`bv_decide` should support matches on multiple enum values at once

Currently bv_decide only understands matches on one enum at a time such as:

inductive Foo where
  | a
  | b
  | c

def isA (f : Foo) : Bool :=
  match f with
  | .a => true
  | _ => false

It does not yet understand something like:

def bothA (f1 f2 : Foo) : Bool :=
  match f1, f2 with
  | .a, .a => true
  | _, _ => false

as detecting and deriving the proper if statements for all situations that occur in multi value pattern matches is much less trivial.

Start by locating the implementation and tests for bv_decide, then trace how it handles single-value enum matches. Define coverage for the shown multi-value pattern and the other multi-pattern situations mentioned in the issue; done means these matches are handled correctly with regression tests.