proposition: Lemma FieldInDg_rac_pivots_1: forall p h pivot pivots f dg, FieldInDg_rac p h (LocSet.add pivot pivots) f dg -> FieldInDg_rac p h pivots f dg.
proof: Proof. intuition. induction H. apply FieldInDg_rac_step with dg';trivial. apply FieldInDg_rac_static;trivial. apply FieldInDg_rac_dynamic with pivot0;trivial. auto with *. apply FieldInDg_rac_same;trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)