Last change
on this file since 3257 was
2716,
checked in by sacerdot, 7 years ago

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

File size:
604 bytes

Line  

1  include "basics/deqsets.ma". 

2  include "basics/lists/listb.ma". 

3  include "ASM/Util.ma". 

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. 

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.