proposition: Lemma init_field_value_not_ref: forall f r, init_field_value f <> Ref r.
proof: Proof. intros. intro. unfold init_field_value in H. destruct (FIELD.initValue f). destruct e; try discriminate H; try destruct l; try discriminate H; try destruct b; try discriminate H; elim init_value_not_ref with f r; trivial. elim init_value_not_ref with f r; trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)