source: src/utilities/bool.ma @ 2327

Last change on this file since 2327 was 2314, checked in by campbell, 8 years ago

Move generic definitions from recent commit to appropriate places.

File size: 205 bytes
Line 
1include "basics/bool.ma".
2include "ASM/Util.ma".
3
4lemma 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/
9qed.
Note: See TracBrowser for help on using the repository browser.