diff options
author | 2016-04-20 18:43:43 -0400 | |
---|---|---|
committer | 2016-06-22 13:44:45 -0400 | |
commit | d46a62e6a9095a7c1c79ee53e069e276958c7613 (patch) | |
tree | 25b2f49433b4a7b535e9c06e59a57c8c0de90094 /src/Util/ListUtil.v | |
parent | 13fae1a26df4e0366b644d103fc9130fc348ad11 (diff) |
Cleanup of GF25519
Diffstat (limited to 'src/Util/ListUtil.v')
-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 |