fact: Definition valid_b_o_So (m : mem) (b : block) (o : ptrofs) : Prop := Mem.range_perm m b (Ptrofs.unsigned o) (Ptrofs.unsigned o + 2) Cur Nonempty.
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