source:
src/utilities/bool.ma
@
2407
| Last change on this file since 2407 was 2314, checked in by , 9 years ago | |
|---|---|
| File size: 205 bytes | |
| Line | |
|---|---|
| 1 | include "basics/bool.ma". |
| 2 | include "ASM/Util.ma". |
| 3 | |
| 4 | lemma if_elim : ∀T:Type[0]. ∀b:bool. ∀e1,e2:T. ∀P:T → Type[0]. |
| 5 | (b → P e1) → |
| 6 | (¬b → P e2) → |
| 7 | P (if b then e1 else e2). |
| 8 | #T * /2/ |
| 9 | qed. |
Note: See TracBrowser
for help on using the repository browser.
