include "basics/bool.ma".
include "ASM/Util.ma".

lemma if_elim : ∀T:Type[0]. ∀b:bool. ∀e1,e2:T. ∀P:T → Type[0].
  (b → P e1) →
  (¬b → P e2) →
  P (if b then e1 else e2).
#T * /2/
qed.