source: src/utilities/listb.ma @ 2474

Last change on this file since 2474 was 2314, checked in by campbell, 8 years ago

Move generic definitions from recent commit to appropriate places.

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.