Last change
on this file since 2751 was
2716,
checked in by sacerdot, 8 years ago

utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction

File size:
604 bytes

Rev  Line  

[2296]  1  include "basics/deqsets.ma". 

[2443]  2  include "basics/lists/listb.ma". 

 3  include "ASM/Util.ma". 

[2296]  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. 

[2443]  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.