source: src/utilities/listb_extra.ma @ 2896

Last change on this file since 2896 was 2728, checked in by sacerdot, 7 years ago

listb.ma => listb_extra.ma for extraction

File size: 381 bytes
Line 
1include "basics/lists/listb.ma".
2include "ASM/Util.ma".
3
4lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
5  Exists S (λy. y = x) l →
6  x ∈ l.
7#S #x #l elim l
8[ //
9| #h #t #IH
10  normalize lapply (eqb_true … x h)
11  cases (x==h) *
12  [ #E #_ >(E (refl ??)) //
13  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
14            | #H @IH @H
15            ]
16  ]
17] qed.
18
Note: See TracBrowser for help on using the repository browser.