- [ { "term inverse relocation" * } {
- [ "delift ( ? ⊢ ? [?,?] ≡ ? )" "delift_lift" * ]
+ [ { "basic local env. thinning" * } {
+ [ "thin ( ? [?,?] ≡ ? )" "thin_ldrop" "thin_delift" * ]
+ }
+ ]
+ [ { "inverse basic term relocation" * } {
+ [ "delift ( ? ⊢ ? [?,?] ≡ ? )" "delift_alt ( ? ⊢ ? [?,?] ≡≡ ? )" "delift_lift" "delift_tpss" "delift_ltpss" "delift_delift" * ]