include "ground_2/relocation/rtmap_sle.ma".
include "basic_2/notation/relations/relationstar_5.ma".
-include "basic_2/grammar/lenv.ma".
+include "basic_2/syntax/lenv.ma".
(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
interpretation "generic entrywise extension (local environment)"
'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2).
-definition lexs_pw_confluent2_R: relation3 lenv term term → relation3 lenv term term →
+definition R_pw_confluent2_lexs: relation3 lenv term term → relation3 lenv term term →
relation3 lenv term term → relation3 lenv term term →
relation3 lenv term term → relation3 lenv term term →
relation3 rtmap lenv term ≝