(**************************************************************************)
include "basic_2/notation/relations/lsubeqx_6.ma".
(**************************************************************************)
include "basic_2/notation/relations/lsubeqx_6.ma".
(* Basic_2A1: uses: lcosx *)
inductive lsubsx (h) (o) (G): rtmap → relation lenv ≝
| lsubsx_atom: ∀f. lsubsx h o G f (⋆) (⋆)
(* Basic_2A1: uses: lcosx *)
inductive lsubsx (h) (o) (G): rtmap → relation lenv ≝
| lsubsx_atom: ∀f. lsubsx h o G f (⋆) (⋆)