1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1/A/defs.ma".
19 include "basic_1/G/defs.ma".
26 inductive leqz: A \to (A \to Prop) \def
27 | leqz_sort: \forall (h1: nat).(\forall (h2: nat).(\forall (n1: nat).(\forall
28 (n2: nat).((eq nat (plus h1 n2) (plus h2 n1)) \to (leqz (ASort h1 n1) (ASort
30 | leqz_head: \forall (a1: A).(\forall (a2: A).((leqz a1 a2) \to (\forall (a3:
31 A).(\forall (a4: A).((leqz a3 a4) \to (leqz (AHead a1 a3) (AHead a2 a4))))))).