(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **************)
definition lex (R): relation lenv ≝
- λL1,L2. â\88\83â\88\83f. ð\9d\90\88â\9dªfâ\9d« & L1 ⪤[cfull,cext2 R,f] L2.
+ λL1,L2. â\88\83â\88\83f. ð\9d\90\88â\9d¨fâ\9d© & L1 ⪤[cfull,cext2 R,f] L2.
interpretation "generic extension (local environment)"
'Relation R L1 L2 = (lex R L1 L2).