+ [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_da" + "aaa_ssta" + "aaa_aaa" * ]
+ }
+ ]
+ [ { "stratified static type assignment" * } {
+ [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ssta" * ]
+ }
+ ]
+ [ { "local env. ref. for degree assignment" * } {
+ [ "lsubd ( ? ⊢ ? ▪⊑ ? )" "lsubd_da" + "lsubd_lsubd" * ]
+ }
+ ]
+ [ { "degree assignment" * } {
+ [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_da" * ]