proposition: Lemma shr_interp: forall bs1 bs2, RAWBITVECTOR_LIST.shr_be (map (Lit.interp rho) bs1) bs2 = map (Lit.interp rho) (shr_lit_be bs1 bs2).
proof: Proof. intros. unfold RAWBITVECTOR_LIST.shr_be, shr_lit_be. now rewrite nshr_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