- [ [ "evaluation for terms" ] "cprre ( ❪?,?❫ ⊢ ? ➡*[?] 𝐍❪?❫ )" "cprre_csx" + "cprre_cpms" + "cprre_cprre" * ]
- [ [ "for lenvs on all entries" ] "lprs ( ❪?,?❫ ⊢ ➡*[?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ]
- [ [ "for binders" ] "cprs_ext" + "( ❪?,?❫ ⊢ ? ➡*[?] ?)" * ]
- [ [ "for terms" ] "cprs" + "( ❪?,?❫ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_tweq" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cnr" + "cprs_cprs" * ]
+ [ [ "evaluation for terms" ] "cprre" "cprre_csx" + "cprre_cpms" + "cprre_cprre" * ]
+ [ [ "for lenvs on all entries" ] "lprs ( ❪?,?❫ ⊢ ➡*[?,?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ]
+ [ [ "for binders" ] "cprs_ext" + "( ❪?,?❫ ⊢ ? ➡*[?,?] ?)" * ]
+ [ [ "for terms" ] "cprs" "cprs_ctc" + "cprs_tweq" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cnr" + "cprs_cprs" * ]