source:
src/utilities/bool.ma
@
2407
| Last change on this file since 2407 was 2314, checked in by , 8 years ago | |
|---|---|
| File size: 205 bytes | |
| Rev | Line | |
|---|---|---|
| [2314] | 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.
