proposition: Lemma isPivot_PivotField: forall p loc, isPivot p loc = true <-> PivotField p loc.
proof: Proof. intros. split; intros. unfold isPivot in H. case_eq loc; intros; rewrite H0 in H; try discriminate H. case_eq (findField p f); intros; rewrite H1 in H. case_eq (FIELD.dataGroups f0); intros; rewrite H2 in H. discriminate H. assert (forall dg , In dg (t :: l) -> In dg (FIELD.dataGroups f0)). intuition. rewrite H2 in |- *. trivial. clear H2. induction (t :: l). discriminate H. case_eq (DATA_GROUP.isDynamic a); intros. apply PivotField_def with f o f0 a; trivial. apply H3. auto with *. apply IHl0. simpl in H. rewrite H2 in H. unfold orb in H. trivial. intros. apply H3. auto with *. discriminate H. destruct H. unfold isPivot in |- *. rewrite H in |- *. rewrite H0 in |- *. induction (FIELD.dataGroups f). elim H1. simpl in H1. destruct H1. subst. simpl in |- *. rewrite H2 in |- *. progress trivial. simpl in |- *. destruct (DATA_GROUP.isDynamic a); trivial. simpl in |- *. apply IHl; trivial. Qed.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)