proposition: Lemma shr_lit_empty: forall b, shr_lit_be [] b = [].
proof: Proof. intro b. unfold shr_lit_be. now rewrite nshr_lit_empty. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance