proposition: Lemma bv_shr_empty: forall b, RAWBITVECTOR_LIST.bv_shr [] b = [].
proof: Proof. intro b. unfold RAWBITVECTOR_LIST.bv_shr. case_eq b; simpl; intros. unfold RAWBITVECTOR_LIST.shr_be. now rewrite rawbv_nshr_empty. unfold RAWBITVECTOR_LIST.size. simpl. unfold RAWBITVECTOR_LIST.zeros. now simpl. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance