(* This file was automatically generated: do not edit *********************)
-
-
-include "aplus/defs.ma".
+include "LambdaDelta-1/aplus/defs.ma".
inductive leq (g: G): A \to (A \to Prop) \def
| leq_sort: \forall (h1: nat).(\forall (h2: nat).(\forall (n1: nat).(\forall