juniorxxue

subst-3m : ∀ k₁ k₂ k₃ es {Γ A B e e₁ j}
  → len es < k₁
  → size j < k₂
  → size-t B < k₃
  → Γ , A ⊢d j # e ▻ (es ⇈) ⦂ B
  → Γ ⊢d ♭ Z # e₁ ⦂ A
  → Γ ⊢d j # ((ƛ e) · e₁) ▻ es ⦂ B
subst-3m (suc k₁) (suc k₂) (suc k₃) [] sz₁ sz₂ sz₃ ⊢1 ⊢2 = ⊢d-app⇒ (⊢d-lam₂ ⊢1) ⊢2
subst-3m (suc k₁) (suc k₂) (suc k₃) (e ∷ es) {j = j} sz₁ sz₂ sz₃ ⊢1 ⊢2 =
  case lst-destruct-rev (e ∷ es) (ees>0 {e} {es}) of λ where

juniorxxue

.tocset {
    position: fixed !important;
    overflow-y: scroll;
    max-height: 100%;
}

juniorxxue

<!-- example 1 - using absolute position for center -->
<nav class="navbar navbar-expand-md navbar-dark bg-primary">
    <a class="navbar-brand abs" href="#">Navbar 1</a>
    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#collapsingNavbar">
        <span class="navbar-toggler-icon"></span>
    </button>
    <div class="navbar-collapse collapse" id="collapsingNavbar">
        <ul class="navbar-nav">
            <li class="nav-item active">
                <a class="nav-link" href="#">Link</a>