[ [ "for binders" ] "cpce_ext" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ]
[ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" "cpce_drops" * ]
}
[ [ "for binders" ] "cpce_ext" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ]
[ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" "cpce_drops" * ]
}