proposition: Lemma PivotTargets_not_nil: forall p pivot, PivotField p pivot -> exists fsig , In fsig (PivotTargets p pivot).
proof: Proof. intros. inversion H. unfold PivotTargets. rewrite H0. rewrite H1. case_eq (DATA_GROUP.pivotTarget dg);intros. destruct d. exists fsig0. apply some_list_list. apply in_map_iff. exists dg. rewrite H4. split; trivial. apply filter_In. tauto. unfold DATA_GROUP.isDynamic in H3. rewrite H4 in H3. inversion H3. 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)