(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
definition cpcs: relation4 genv lenv term term ≝
(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
definition cpcs: relation4 genv lenv term term ≝
interpretation "context-sensitive parallel equivalence (term)"
'PConvStar G L T1 T2 = (cpcs G L T1 T2).
interpretation "context-sensitive parallel equivalence (term)"
'PConvStar G L T1 T2 = (cpcs G L T1 T2).