source: src/utilities/deqsets.ma @ 2300

Last change on this file since 2300 was 2296, checked in by campbell, 9 years ago

Tidy up some ill-placed definitions.
File size: 311 bytes
Line 
1include "basics/deqsets.ma".
2
3lemma 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.