Changeset 1351 for src/utilities/lists.ma
 Timestamp:
 Oct 11, 2011, 12:24:33 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/lists.ma
r1316 r1351 91 91 #h #t #IH * [ #H #F %1 @F @H  #H #F %2 @IH [ @H  @F ] ] qed. 92 92 93 lemma Exists_exists : ∀A,P,l. 94 Exists A P l → 95 ∃x. P x. 96 #A #P #l elim l [ *  #hd #tl #IH * [ #H %{hd} @H  @IH ] 97 qed. 98 99 lemma Exists_All : ∀A,P,Q,l. 100 Exists A P l → 101 All A Q l → 102 ∃x. P x ∧ Q x. 103 #A #P #Q #l elim l [ *  #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/  #H1 * #_ #H2 @IH // ] 104 qed. 105 93 106 lemma map_append : ∀A,B,f,l1,l2. 94 107 (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
Note: See TracChangeset
for help on using the changeset viewer.