Changeset 990 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Jun 17, 2011, 1:30:01 PM (8 years ago)
Author:
sacerdot
Message:

Do no longer use the daemon automatically :-)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r985 r990  
    3030lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
    3131 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
    32  #n #hd #tl #abs @⊥ //
     32 #n #hd #tl #abs @⊥ destruct (abs)
    3333qed.
    3434
     
    3636 ∃hd.∃tl.v ≃ VCons bool n hd tl.
    3737 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
    38  [ #abs @⊥ //
     38 [ #abs @⊥ destruct (abs)
    3939 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
    4040qed.
Note: See TracChangeset for help on using the changeset viewer.