Changeset 1631 for src/utilities/lists.ma
 Timestamp:
 Dec 19, 2011, 2:48:37 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/lists.ma
r1630 r1631 5 5 [ // 6 6  #hd #tl #IH #r * #H1 #H2 #H3 % // @IH // 7 ] qed. 7 ] qed. 8 9 lemma All_append_l : ∀A,P,l,r. All A P (l@r) → All A P l. 10 #A #P #l elim l 11 [ // 12  #hd #tl #IH #r * #H1 #H2 % /2/ 13 ] qed. 14 15 lemma All_append_r : ∀A,P,l,r. All A P (l@r) → All A P r. 16 #A #P #l elim l 17 [ // 18  #h #t #IH #r * /2/ 19 ] qed. 8 20 9 21 (* An alternative form of All that can be easier to use sometimes. *)
Note: See TracChangeset
for help on using the changeset viewer.