|
Last change
on this file since 3129 was
2716,
checked in by sacerdot, 8 years ago
|
|
utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
|
|
File size:
604 bytes
|
| Line | |
|---|
| 1 | include "basics/deqsets.ma". |
|---|
| 2 | include "basics/lists/listb.ma". |
|---|
| 3 | include "ASM/Util.ma". |
|---|
| 4 | |
|---|
| 5 | lemma 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? *) |
|---|
| 16 | lemma 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 | ] |
|---|
| 23 | qed. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
