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