(* BOOLEANI *)
(* ******** *)
-ndefinition bool_destruct :
- Πb1,b2:bool.ΠP:Prop.b1 = b2 →
+ndefinition bool_destruct_aux ≝
+Πb1,b2:bool.ΠP:Prop.b1 = b2 →
match b1 with
[ true ⇒ match b2 with [ true ⇒ P → P | false ⇒ P ]
| false ⇒ match b2 with [ true ⇒ P | false ⇒ P → P ]
].
+
+ndefinition bool_destruct : bool_destruct_aux.
#b1; #b2; #P;
nelim b1;
nelim b2;