inductive lexs (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝
| lexs_atom: ∀f. lexs RN RP f (⋆) (⋆)
| lexs_next: ∀f,I1,I2,L1,L2.
inductive lexs (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝
| lexs_atom: ∀f. lexs RN RP f (⋆) (⋆)
| lexs_next: ∀f,I1,I2,L1,L2.