proposition: Lemma shl_interp: forall bs1 bs2, RAWBITVECTOR_LIST.shl_be (map (Lit.interp rho) bs1) bs2 = map (Lit.interp rho) (shl_lit_be bs1 bs2).
proof: Proof. intros. unfold RAWBITVECTOR_LIST.shl_be, shl_lit_be. now rewrite nshl_interp. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance