Changeset 2897 for src/utilities
 Timestamp:
 Mar 16, 2013, 9:08:21 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/lists.ma
r2800 r2897 109 109  #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hda} //  /2/ ] 110 110 ] qed. 111 112 lemma 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 * // 117 qed. 111 118 112 119 let 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.