diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-20 18:43:43 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-20 18:43:43 -0400 |
| commit | 8720fbfec19d4a4823a5a65771a8122af7e83a09 (patch) | |
| tree | 92db9e79c6a72211c302604d936f0e5d0a3569de /src/Util | |
| parent | 50c72878679fd77a5c5eb04e3c913c195e4e9757 (diff) | |
Cleanup of GF25519
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ListUtil.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 0e061d5e5..b640fb8e8 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -556,3 +556,11 @@ Proof. revert n; induction l; simpl; intro n; destruct n; [ try reflexivity.. ]. nth_tac. Qed. + +Lemma fold_right_and_True_forall_In_iff : forall {T} (l : list T) (P : T -> Prop), + (forall x, In x l -> P x) <-> fold_right and True (map P l). +Proof. + induction l; intros; simpl; try tauto. + rewrite <- IHl. + intuition (subst; auto). +Qed.
\ No newline at end of file |