fact: Definition check_shl (bs1: list _lit) (bs2: list bool) (bsres: list _lit) : bool := if (Nat.eqb (length bs1) (length bs2)) then if (forallb2 eq_carry_lit (lit_to_carry (shl_lit_be bs1 bs2)) bsres) then true else false else false.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance