Changeset 990 for src/ASM/BitVector.ma

Timestamp:

Jun 17, 2011, 1:30:01 PM (10 years ago)

Author:

sacerdot

Message:

Do no longer use the daemon automatically :-)

File:

• src/ASM/BitVector.ma (modified) (2 diffs)

src/ASM/BitVector.ma

@@ -30 +30 @@
 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
  #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
- #n #hd #tl #abs @⊥ //
+ #n #hd #tl #abs @⊥ destruct (abs)
 qed.
 
@@ -36 +36 @@
  ∃hd.∃tl.v ≃ VCons bool n hd tl.
  #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
- [ #abs @⊥ //
+ [ #abs @⊥ destruct (abs)
  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
 qed.