diff --git a/nix/nvim-agda/agda-vim-excerpts/autoload.vim b/nix/nvim-agda/agda-vim-excerpts/autoload.vim
index 48b4bc04..e638176d 100644
--- a/nix/nvim-agda/agda-vim-excerpts/autoload.vim
+++ b/nix/nvim-agda/agda-vim-excerpts/autoload.vim
@@ -10,8 +10,14 @@ if !exists('g:agda#default_glyphs')
   " Extra Shit
   call extend(g:agda#default_glyphs, {
     \   'Gl-': 'ƛ',
+    \   '==': '≡',
+    \   '<': '⟨',
+    \   '>': '⟩',
     \   'em': '—',
     \   '=>': '⇒',
+    \   '~-': '≃',
+    \   'r': '→',
+    \   '0': '∅',
     \})
 
   " Combining marks
@@ -365,16 +371,16 @@ if !exists('g:agda#default_glyphs')
 
   " Subscripts
   call extend(g:agda#default_glyphs, {
-    \   '0': '₀',
-    \   '1': '₁',
-    \   '2': '₂',
-    \   '3': '₃',
-    \   '4': '₄',
-    \   '5': '₅',
-    \   '6': '₆',
-    \   '7': '₇',
-    \   '8': '₈',
-    \   '9': '₉',
+    \   '_0': '₀',
+    \   '_1': '₁',
+    \   '_2': '₂',
+    \   '_3': '₃',
+    \   '_4': '₄',
+    \   '_5': '₅',
+    \   '_6': '₆',
+    \   '_7': '₇',
+    \   '_8': '₈',
+    \   '_9': '₉',
     \   '_a': 'ₐ',
     \   '_e': 'ₑ',
     \   '_h': 'ₕ',
@@ -451,7 +457,6 @@ if !exists('g:agda#default_glyphs')
     \   'pi': 'π',
     \   'p': 'π',
     \   'rho': 'ρ',
-    \   'r': 'ρ',
     \   'sigma': 'σ',
     \   's': 'σ',
     \   'varsigma': 'ς',
diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md
index 0ab9d8f7..1ccc9494 100644
--- a/src/plfa/part2/Lambda.lagda.md
+++ b/src/plfa/part2/Lambda.lagda.md
@@ -1056,7 +1056,34 @@ to the list
     [ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ]
 
 ```
--- Your code goes here
+open import plfa.part1.Isomorphism using (_≃_)
+open import Data.Product using (_×_; _,_)
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning renaming (begin_ to begin-≡_; _∎ to _∎-≡)
+
+contextOfList : (l : List (Id × Type)) →  Context
+contextOfList [] = ∅
+contextOfList ((id , type) ∷ l) = (contextOfList l) , id ⦂ type
+
+listOfContext : (c : Context) →  List (Id × Type)
+listOfContext ∅ = []
+listOfContext (c , x ⦂ x₁) = (x , x₁) ∷ listOfContext c
+
+contextListIso : (c : Context) →  contextOfList (listOfContext c) ≡ c
+contextListIso ∅ = refl
+contextListIso (c , x ⦂ x₁) = cong (_, x ⦂ x₁) (contextListIso c)
+
+listContextIso : (l : List (Id × Type)) →  listOfContext (contextOfList l) ≡ l
+listContextIso [] = refl
+listContextIso (x ∷ l) = cong (x ∷_) (listContextIso l)
+
+Context≃List : Context ≃ List (Id × Type)
+Context≃List = record
+  { from = contextOfList
+  ; to = listOfContext
+  ; from∘to = contextListIso
+  ; to∘from = ?
+  }
 ```
 
 ### Lookup judgment