Changeset 2897 for src/utilities


Ignore:
Timestamp:
Mar 16, 2013, 9:08:21 PM (8 years ago)
Author:
campbell
Message:

Minor tidying.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r2800 r2897  
    109109| #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hda} // | /2/ ]
    110110] qed.
     111
     112lemma All2_tail : ∀A,B,P,a,b.
     113  All2 A B P a b →
     114  All2 A B P (tail A a) (tail B b).
     115#A #B #P * [2: #ah #at] * [2,4: #bh #bt]
     116* //
     117qed.
    111118
    112119let rec map_All (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → B) (l:list A) (H:All A P l) on l : list B ≝
Note: See TracChangeset for help on using the changeset viewer.