Ignore:
Timestamp:
Apr 3, 2013, 5:54:34 PM (7 years ago)
Author:
campbell
Message:

Tidy up recent work a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r2897 r3081  
    7474  | * #p #H whd in ⊢ (?%); >p /2/
    7575  ]
     76] qed.
     77
     78lemma all_append : ∀A,p,l1,l2.
     79  all A p (l1@l2) →
     80  all A p l1 ∧ all A p l2.
     81#A #p #l1 elim l1
     82[ //
     83| #h #t #IH #l2
     84  whd in ⊢ (?% → ?(?%?));
     85  cases (p h) //
     86  @IH
    7687] qed.
    7788
Note: See TracChangeset for help on using the changeset viewer.