proposition: Lemma rawbv_nshr_empty: forall b, RAWBITVECTOR_LIST.nshr_be [] b = [].
proof: Proof. intro b. induction b; intros; 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