source:
src/utilities/deqsets.ma
@
2300
Last change on this file since 2300 was 2296, checked in by , 9 years ago | |
---|---|
File size: 311 bytes |
Line | |
---|---|
1 | include "basics/deqsets.ma". |
2 | |
3 | lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D. |
4 | (x = y → P true) → |
5 | (x ≠ y → P false) → |
6 | P (eqb D x y). |
7 | #D #P #x #y #T #F lapply (eqb_true D x y) cases (eqb D x y) * |
8 | [ #TT #_ @T @TT // |
9 | | #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct |
10 | ] qed. |
Note: See TracBrowser
for help on using the repository browser.