include "basics/deqsets.ma".
include "basics/lists/listb.ma".
include "ASM/Util.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.


(* is it already there? *)
lemma All_memb : ∀A : DeqSet.∀P,l,x.All A P l → x ∈ l → P x.
#A #P #l elim l
[ #x * *
| #hd #tl #IH #x * #Phd #Ptl
  normalize @(eqb_elim A) #H normalize nodelta [destruct * @Phd]
  @IH @Ptl
]
qed.