fact: Definition EvalNonnullElements (e : Expression) (st : State.t) : Prop := forall loc , EvalRefExpression e st = Some loc /\ forall elem index, Heap.get st@h (Heap.ArrayElement loc index) = Some elem -> elem <> Null.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)