fact: Definition bv_or (a b : bitvector) : bitvector := match (@size a) =? (@size b) with | true => map2 orb (@bits a) (@bits b) | _ => nil end.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance