inductive bool : Set \def
| true : bool
| false : bool.
-
+
+theorem bool_elim: \forall P:bool \to Prop. \forall b:bool.
+ (b = true \to P true)
+ \to (b = false \to P false)
+ \to P b.
+ intros 2 (P b).
+ elim b;
+ [ apply H; reflexivity
+ | apply H1; reflexivity
+ ]
+qed.
+
theorem not_eq_true_false : true \neq false.
simplify.intro.
change with