proposition: Lemma FieldInDg_rac_1: forall p h f dg, FieldInDg p h f dg <-> FieldInDg_rac p h LocSet.empty f dg.
proof: Proof. intros. split; intro. induction H. apply FieldInDg_rac_step with dg';trivial. apply FieldInDg_rac_static; trivial. apply FieldInDg_rac_dynamic with pivot; trivial. apply LocSet.empty_1. apply FieldInDg_rac_same; trivial. induction H. apply FieldInDg_step with dg';trivial. apply FieldInDg_static; trivial. apply FieldInDg_dynamic with pivot; trivial. apply FieldInDg_same; trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)