source: src/utilities/deqsets_extra.ma @ 2896

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

utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction

File size: 604 bytes
Line 
1include "basics/deqsets.ma".
2include "basics/lists/listb.ma".
3include "ASM/Util.ma".
4
5lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D.
6  (x = y → P true) →
7  (x ≠ y → P false) →
8  P (eqb D x y).
9#D #P #x #y #T #F lapply (eqb_true D x y) cases (eqb D x y) *
10[ #TT #_ @T @TT //
11| #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct
12] qed.
13
14
15(* is it already there? *)
16lemma All_memb : ∀A : DeqSet.∀P,l,x.All A P l → x ∈ l → P x.
17#A #P #l elim l
18[ #x * *
19| #hd #tl #IH #x * #Phd #Ptl
20  normalize @(eqb_elim A) #H normalize nodelta [destruct * @Phd]
21  @IH @Ptl
22]
23qed.
Note: See TracBrowser for help on using the repository browser.