feat: show an equivalence between bitvectors and Fin w -> Bool

[alexkeizer]

---

[alexkeizer]

Proving the equivalence for the big-endian case is turning out to require a decent number of extra intermediate results, so I figure it's easier to move that to another PR and stub it out for now. Thus, I'm marking this PR ready for review!

[eric-wieser]

Aren't these trivial to prove by induction on w, without invoking the above?

[alexkeizer]

We would need to do induction on x, or at the least, have the result concat (x >>> 1 |>.truncate n) x.lsb = x, for x : BitVec (n+1), but once we do have that I do agree it would be cleaner to just prove it directly.

[eric-wieser]

Do you think it makes more sense to implement this by taking the bitwise or of bif f i then 1 else 0 <<< i using multiset.fold or similar?
If nothing else, it would be nice to prove that those are equal

[alexkeizer]

I considered this, it might be faster since there are then less data-dependencies, but it does complicate proofs.
In particular, we might want to upstream ofLEFn to Std at some point, so I would prefer not to rely to much on Mathlib-specific APIs.

For posterity: the following is an alternative def of ofLEFn that would work.

List.finRange w
    |>.map (fun i =>
        shiftLeftZeroExtend (ofBool (f i)) i.val |>.zeroExtend' (Nat.add_comm _ _ ▸ i.prop)
      )
    |>.foldr (· ||| ·) 0#_