proposition: Lemma valid_b_o_So_dec: forall m b o, {valid_b_o_So m b o} + {~ valid_b_o_So m b o}.
proof: Proof. intros. unfold valid_b_o_So. apply Mem.range_perm_dec. Qed.
imports: compcert.common.Events compcert.common.Memory compcert.common.Values compcert.common.AST compcert.lib.Integers Coq.ZArith.BinInt Coq.Lists.List Coq.micromega.Lia