Link activation

[FissoreD]

• [ ] eta-link
  • [x] eta-progress-lhs
  • [x] eta-progress-rhs
  • [ ] eta-progress-dedup
• [x] llam-link $\Gamma \vdash T =_L app[X|L]$
  • [x] llam-progress-rhs : $X$ becomes a rigid term
  • [x] llam-refine $L.(0)$ becomes a names which is not in the scope of $X$
  • [ ] scope-check
  • [x] eta
  • [ ] llam