Changeset 1105 for Deliverables/D3.3/idlookupbranch/utilities
 Timestamp:
 Aug 10, 2011, 5:17:58 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/utilities/lists.ma
r1102 r1105 17 17 #h #t #IH * /3/ 18 18 qed. 19 20 lemma All_nth : ∀A,P,n,l. 21 All A P l → 22 ∀a. 23 nth_opt A n l = Some A a → 24 P a. 25 #A #P #n elim n 26 [ * [ #_ #a #E whd in E:(??%?); destruct 27  #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H 28 ] 29  #m #IH * 30 [ #_ #a #E whd in E:(??%?); destruct 31  #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?) @IH 32 ] 33 ] qed. 19 34 20 35 let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
Note: See TracChangeset
for help on using the changeset viewer.