Ignore:
Timestamp:
Oct 11, 2011, 12:24:33 PM (9 years ago)
Author:
campbell
Message:

Tidy up some loose ends from the invariants branch merge.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r1316 r1351  
    9191#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
    9292
     93lemma 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 ]
     97qed.
     98
     99lemma 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 // ]
     104qed.
     105
    93106lemma map_append : ∀A,B,f,l1,l2.
    94107  (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.