# package:sbv

( # ) :: forall (n :: Nat) bv (m :: Nat) . (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m)) => SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
sbv Data.SBV
Join two bitvectors. 
>>> prove $ \x y -> x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71))
Q.E.D.
( # ) :: forall (n :: Nat) bv (m :: Nat) . (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m)) => SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
sbv Data.SBV.Internals Data.SBV.Trans
Join two bitvectors.