proposition: Lemma FieldInDg_rac2_Correct: forall p h ep1 ep2 f dg, ep1 [=] ep2 -> (Rac2.FieldInDg_rac p h ep1 f dg <-> FieldInDg_rac2 p h ep2 (LocSet.singleton f) f dg).
proof: Proof. Admitted. Lemma FieldInDg_rac2_EqualSet: forall p h ep s1 f dg, FieldInDg_rac2 p h ep s1 f dg -> forall s2, s1 [=] s2 -> FieldInDg_rac2 p h ep s2 f dg. Proof. intros p h ep s1 f dg H. induction H. intros. apply FieldInDg_rac2_static with dg'; trivial. intro; elim H0. apply H2. trivial. apply IHFieldInDg_rac2. auto with *. intros. apply FieldInDg_rac2_dynamic with pivot dg'; trivial. intro; elim H1. apply H3. trivial. apply IHFieldInDg_rac2. auto with *. intros. apply FieldInDg_rac2_base; trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)