From d46a62e6a9095a7c1c79ee53e069e276958c7613 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 20 Apr 2016 18:43:43 -0400 Subject: Cleanup of GF25519 --- src/Util/ListUtil.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/Util/ListUtil.v') 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 -- cgit v1.2.3