proposition: Lemma StaticDGs_Correct: forall p field_am dg_am, In dg_am (StaticDGs p field_am) <-> direct_FieldInDg_static p field_am dg_am.
proof: Proof. intuition. unfold StaticDGs in H. case_eq field_am; intros; subst; try inversion H. case_eq (findField p f); intros; rewrite H0 in H; try inversion H. apply in_map_iff in H. destruct H as [dg_fsig H]. destruct H. apply in_flat_map in H1. destruct H1 as [dg H1]. destruct H1. apply filter_In in H1. destruct H1. split with o dg_fsig o f f0 dg; auto. case_eq (DATA_GROUP.isDynamic dg); intros. rewrite H4 in H3; inversion H3. trivial. destruct H. unfold StaticDGs. rewrite H0. rewrite H2. apply in_map_iff. exists dg_fsig. rewrite <- H1. split; auto. apply in_flat_map. exists dg. rewrite filter_In. split. split. trivial. rewrite H4. simpl; trivial. 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)