1 files changed, 100 insertions, 16 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 5d8f98ed..c17b285b 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,24 +1,108 @@
-le_S: forall n m : nat, n <= m -> n <= S m
 le_n: forall n : nat, n <= n
-le_pred: forall n m : nat, n <= m -> pred n <= pred m
+le_S: forall n m : nat, n <= m -> n <= S m
+le_ind:
+  forall (n : nat) (P : nat -> Prop),
+  P n ->
+  (forall m : nat, n <= m -> P m -> P (S m)) ->
+  forall n0 : nat, n <= n0 -> P n0
+le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
-false: bool
+le_0_n: forall n : nat, 0 <= n
+le_n_S: forall n m : nat, n <= m -> S n <= S m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
 true: bool
-xorb: bool -> bool -> bool
+false: bool
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
+bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
+andb: bool -> bool -> bool
 orb: bool -> bool -> bool
-negb: bool -> bool
 implb: bool -> bool -> bool
-andb: bool -> bool -> bool
-pred_Sn: forall n : nat, n = pred (S n)
-plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+xorb: bool -> bool -> bool
+negb: bool -> bool
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+andb_true_intro:
+  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+eq_true: bool -> Prop
+eq_true_rect:
+  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
+eq_true_rec:
+  forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
+is_true: bool -> Prop
+eq_true_ind_r:
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+eq_true_rec_r:
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_rect_r:
+  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
+BoolSpec: Prop -> Prop -> bool -> Prop
+BoolSpec_ind:
+  forall (P Q : Prop) (P0 : bool -> Prop),
+  (P -> P0 true) ->
+  (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
+Nat.eqb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.even: nat -> bool
+Nat.odd: nat -> bool
+Nat.testbit: nat -> nat -> bool
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+bool_choice:
+  forall (S : Set) (R1 R2 : S -> Prop),
+  (forall x : S, {R1 x} + {R2 x}) ->
+  {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
+eq_S: forall x y : nat, x = y -> S x = S y
+f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+pred_Sn: forall n : nat, n = Nat.pred (S n)
+eq_add_S: forall n m : nat, S n = S m -> n = m
+not_eq_S: forall n m : nat, n <> m -> S n <> S m
+O_S: forall n : nat, 0 <> S n
+n_Sn: forall n : nat, n <> S n
+f_equal2_plus:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+f_equal2_nat:
+  forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
+  x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
 plus_n_O: forall n : nat, n = n + 0
-plus_Sn_m: forall n m : nat, S n + m = S (n + m)
 plus_O_n: forall n : nat, 0 + n = n
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+f_equal2_mult:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
 mult_n_O: forall n : nat, 0 = n * 0
-min_r: forall n m : nat, m <= n -> min n m = m
-min_l: forall n m : nat, n <= m -> min n m = n
-max_r: forall n m : nat, n <= m -> max n m = m
-max_l: forall n m : nat, m <= n -> max n m = n
-eq_add_S: forall n m : nat, S n = S m -> n = m
-eq_S: forall x y : nat, x = y -> S x = S y
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+andb_true_intro:
+  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+bool_choice:
+  forall (S : Set) (R1 R2 : S -> Prop),
+  (forall x : S, {R1 x} + {R2 x}) ->
+  {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+andb_true_intro:
+  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+h': newdef n <> n
+h: n <> newdef n
+h': newdef n <> n
+h: n <> newdef n
+h: n <> newdef n
+h: n <> newdef n
+h': ~ P n
+h: P n
+h': ~ P n
+h: P n
+h': ~ P n
+h: P n
+h: P n
+h: P n