interpretation "generic entrywise extension (local environment)"
'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2).
interpretation "generic entrywise extension (local environment)"
'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2).
relation3 lenv term term → relation3 lenv term term →
relation3 lenv term term → relation3 lenv term term →
relation3 rtmap lenv term ≝
relation3 lenv term term → relation3 lenv term term →
relation3 lenv term term → relation3 lenv term term →
relation3 rtmap lenv term ≝