fact: Fixpoint nshl_lit_be (a: list _lit) (n: nat): list _lit := match n with | O => a | S n' => nshl_lit_be (_shl_lit_be a) n' end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance