proposition: Lemma nshr_interp: forall n bs1, RAWBITVECTOR_LIST.nshr_be (map (Lit.interp rho) bs1) n = map (Lit.interp rho) (nshr_lit_be bs1 n).
proof: Proof. intro n. induction n; intros. - now simpl. - simpl. specialize (@IHn (_shr_lit_be bs1)). rewrite <- IHn. simpl. now rewrite prop_shr_be. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance