Changeset 990 for src/ASM/BitVector.ma
- Timestamp:
- Jun 17, 2011, 1:30:01 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/BitVector.ma
r985 r990 30 30 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. 31 31 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // 32 #n #hd #tl #abs @⊥ //32 #n #hd #tl #abs @⊥ destruct (abs) 33 33 qed. 34 34 … … 36 36 ∃hd.∃tl.v ≃ VCons bool n hd tl. 37 37 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) 38 [ #abs @⊥ //38 [ #abs @⊥ destruct (abs) 39 39 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] 40 40 qed.
Note: See TracChangeset
for help on using the changeset viewer.