Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (8 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/deqsets.ma

    r2296 r2443  
    11include "basics/deqsets.ma".
     2include "basics/lists/listb.ma".
     3include "ASM/Util.ma".
    24
    35lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D.
     
    911| #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct
    1012] qed.
     13
     14
     15(* is it already there? *)
     16lemma 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]
     23qed.
Note: See TracChangeset for help on using the changeset viewer.