fact: Definition shl_lit_be (a: list _lit) (b: list bool): list _lit := nshl_lit_be a (RAWBITVECTOR_LIST.list2nat_be b).
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance