fact: Definition bitwise_or n v1 v2 : Vector.t bool n := vector_double_rect bool (fun n v1 v2 => Vector.t bool n) Vector.nil (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat Bool