include "basics/deqsets.ma".

lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D.
  (x = y → P true) →
  (x ≠ y → P false) →
  P (eqb D x y).
#D #P #x #y #T #F lapply (eqb_true D x y) cases (eqb D x y) *
[ #TT #_ @T @TT //
| #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct
] qed.