(****************************************************************************)
(*                                                                          *)
(*                The formal system \lambda\delta                           *)
(*                                                                          *)
(*                Author: Ferruccio Guidi                                   *)
(*                                                                          *)
(*                This file is distributed under the terms of the           *)
(*                GNU General Public License Version 2                      *)
(*                                                                          *)
(****************************************************************************)

Require Export Arith.
Require Export Wf_nat.

(* eq ***********************************************************************)

      Hint eq : ld := Constructors eq.

      Hint f1N : ld := Resolve (f_equal nat).

      Hint f2NN : ld := Resolve (f_equal2 nat nat).

      Hints Resolve plus_n_O plus_sym plus_n_Sm plus_assoc_r : ld.

      Hints Resolve minus_n_O : ld.

(* le ***********************************************************************)

      Hint le : ld := Constructors le.

      Hints Resolve le_O_n le_n_S le_pred_n : ld.

      Hints Resolve le_plus_plus le_plus_trans le_plus_l le_plus_r : ld.

(* lt ***********************************************************************)

      Hints Unfold lt : ld.

      Hints Resolve lt_n_S : ld.

      Hints Resolve lt_reg_l lt_reg_r lt_le_plus_plus le_lt_plus_plus : ld.

      Hints Resolve lt_plus_plus : ld.

(* not **********************************************************************)

      Hints Resolve O_S not_eq_S : ld.