agda: Clean up formatting

hazelgrove · Sep 30, 2023 · c57371f · c57371f
1 parent c489a9c
commit c57371f
Show file tree

Hide file tree

Showing 9 changed files with 199 additions and 191 deletions.
diff --git a/hazelnut/action.agda b/hazelnut/action.agda
@@ -68,40 +68,40 @@ module hazelnut.action where
 
     data _eshape : Shape → Set where
       ASortVar   : (x : Var)
-              → (var x) eshape
+                 → (var x) eshape
       ASortLam   : (x : Var)
-              → (lam x) eshape
+                 → (lam x) eshape
       ASortAp₁   : (u : Hole)
-              → (ap₁ u) eshape
+                 → (ap₁ u) eshape
       ASortAp₂   : (u : Hole)
-              → (ap₂ u) eshape
+                 → (ap₂ u) eshape
       ASortLet₁  : (x : Var)
-              → (u : Hole)
-              → (let₁ x u) eshape
+                 → (u : Hole)
+                 → (let₁ x u) eshape
       ASortLet₂  : (x : Var)
-              → (u : Hole)
-              → (let₂ x u) eshape
+                 → (u : Hole)
+                 → (let₂ x u) eshape
       ASortNum   : (n : ℕ)
-              → (num n) eshape
+                 → (num n) eshape
       ASortPlus₁ : (u : Hole)
-              → (plus₁ u) eshape
+                 → (plus₁ u) eshape
       ASortPlus₂ : (u : Hole)
-              → (plus₂ u) eshape
+                 → (plus₂ u) eshape
       ASortTrue  : tt eshape
       ASortFalse : ff eshape
       ASortIf₁   : (u₁ : Hole)
-              → (u₂ : Hole)
-              → (if₁ u₁ u₂) eshape
+                 → (u₂ : Hole)
+                 → (if₁ u₁ u₂) eshape
       ASortIf₂   : (u₁ : Hole)
-              → (u₂ : Hole)
-              → (if₂ u₁ u₂) eshape
+                 → (u₂ : Hole)
+                 → (if₂ u₁ u₂) eshape
       ASortIf₃   : (u₁ : Hole)
-              → (u₂ : Hole)
-              → (if₃ u₁ u₂) eshape
+                 → (u₂ : Hole)
+                 → (if₃ u₁ u₂) eshape
       ASortPair₁ : (u : Hole)
-              → (pair₁ u) eshape
+                 → (pair₁ u) eshape
       ASortPair₂ : (u : Hole)
-              → (pair₂ u) eshape
+                 → (pair₂ u) eshape
       ASortProjL : projl eshape
       ASortProjR : projr eshape
 

diff --git a/hazelnut/untyped/action.agda b/hazelnut/untyped/action.agda
@@ -58,32 +58,32 @@ module hazelnut.untyped.action where
   -- expression actions
   data _+_+e>_ : (ê : ZExp) → (α : Action) → (ê′ : ZExp) → Set where
     -- movement
-    AEMLamChild1  : ∀ {x τ e}
-                  → ‵▹ ‵λ x ∶ τ ∙ e ◃ + move (child 1) +e> (‵λ₁ x ∶ ▹ τ ◃ ∙ e)
-    AEMLamChild2  : ∀ {x τ e}
-                  → ‵▹ ‵λ x ∶ τ ∙ e ◃ + move (child 2) +e> (‵λ₂ x ∶ τ ∙ ‵▹ e ◃)
-    AEMLamParent1 : ∀ {x τ e}
-                  → (‵λ₁ x ∶ ▹ τ ◃ ∙ e) + move parent +e> ‵▹ ‵λ x ∶ τ ∙ e ◃
-    AEMLamParent2 : ∀ {x τ e}
-                  → (‵λ₂ x ∶ τ ∙ ‵▹ e ◃) + move parent +e> ‵▹ ‵λ x ∶ τ ∙ e ◃
-
-    AEMApChild1  : ∀ {e₁ e₂}
-                 → ‵▹ ‵ e₁ ∙ e₂ ◃ + move (child 1) +e> (‵ ‵▹ e₁ ◃ ∙₁ e₂)
-    AEMApChild2  : ∀ {e₁ e₂}
-                 → ‵▹ ‵ e₁ ∙ e₂ ◃ + move (child 2) +e> (‵ e₁ ∙₂ ‵▹ e₂ ◃)
-    AEMApParent1 : ∀ {e₁ e₂}
-                 → (‵ ‵▹ e₁ ◃ ∙₁ e₂) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ◃
-    AEMApParent2 : ∀ {e₁ e₂}
-                 → (‵ e₁ ∙₂ ‵▹ e₂ ◃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ◃
-
-    AEMLetChild1  : ∀ {x e₁ e₂}
-                  → ‵▹ ‵ x ← e₁ ∙ e₂ ◃ + move (child 1) +e> (‵ x ←₁ ‵▹ e₁ ◃ ∙ e₂)
-    AEMLetChild2  : ∀ {x e₁ e₂}
-                  → ‵▹ ‵ x ← e₁ ∙ e₂ ◃ + move (child 2) +e> (‵ x ←₂ e₁ ∙ ‵▹ e₂ ◃)
-    AEMLetParent1 : ∀ {x e₁ e₂}
-                  → (‵ x ←₁ ‵▹ e₁ ◃ ∙ e₂) + move parent +e> ‵▹ ‵ x ← e₁ ∙ e₂ ◃
-    AEMLetParent2 : ∀ {x e₁ e₂}
-                  → (‵ x ←₂ e₁ ∙ ‵▹ e₂ ◃) + move parent +e> ‵▹ ‵ x ← e₁ ∙ e₂ ◃
+    AEMLamChild1   : ∀ {x τ e}
+                   → ‵▹ ‵λ x ∶ τ ∙ e ◃ + move (child 1) +e> (‵λ₁ x ∶ ▹ τ ◃ ∙ e)
+    AEMLamChild2   : ∀ {x τ e}
+                   → ‵▹ ‵λ x ∶ τ ∙ e ◃ + move (child 2) +e> (‵λ₂ x ∶ τ ∙ ‵▹ e ◃)
+    AEMLamParent1  : ∀ {x τ e}
+                   → (‵λ₁ x ∶ ▹ τ ◃ ∙ e) + move parent +e> ‵▹ ‵λ x ∶ τ ∙ e ◃
+    AEMLamParent2  : ∀ {x τ e}
+                   → (‵λ₂ x ∶ τ ∙ ‵▹ e ◃) + move parent +e> ‵▹ ‵λ x ∶ τ ∙ e ◃
+
+    AEMApChild1    : ∀ {e₁ e₂}
+                   → ‵▹ ‵ e₁ ∙ e₂ ◃ + move (child 1) +e> (‵ ‵▹ e₁ ◃ ∙₁ e₂)
+    AEMApChild2    : ∀ {e₁ e₂}
+                   → ‵▹ ‵ e₁ ∙ e₂ ◃ + move (child 2) +e> (‵ e₁ ∙₂ ‵▹ e₂ ◃)
+    AEMApParent1   : ∀ {e₁ e₂}
+                   → (‵ ‵▹ e₁ ◃ ∙₁ e₂) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ◃
+    AEMApParent2   : ∀ {e₁ e₂}
+                   → (‵ e₁ ∙₂ ‵▹ e₂ ◃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ◃
+
+    AEMLetChild1   : ∀ {x e₁ e₂}
+                   → ‵▹ ‵ x ← e₁ ∙ e₂ ◃ + move (child 1) +e> (‵ x ←₁ ‵▹ e₁ ◃ ∙ e₂)
+    AEMLetChild2   : ∀ {x e₁ e₂}
+                   → ‵▹ ‵ x ← e₁ ∙ e₂ ◃ + move (child 2) +e> (‵ x ←₂ e₁ ∙ ‵▹ e₂ ◃)
+    AEMLetParent1  : ∀ {x e₁ e₂}
+                   → (‵ x ←₁ ‵▹ e₁ ◃ ∙ e₂) + move parent +e> ‵▹ ‵ x ← e₁ ∙ e₂ ◃
+    AEMLetParent2  : ∀ {x e₁ e₂}
+                   → (‵ x ←₂ e₁ ∙ ‵▹ e₂ ◃) + move parent +e> ‵▹ ‵ x ← e₁ ∙ e₂ ◃
 
     AEMPlusChild1  : ∀ {e₁ e₂}
                    → ‵▹ ‵ e₁ + e₂ ◃ + move (child 1) +e> (‵ ‵▹ e₁ ◃ +₁ e₂)
@@ -94,36 +94,36 @@ module hazelnut.untyped.action where
     AEMPlusParent2 : ∀ {e₁ e₂}
                    → (‵ e₁ +₂ ‵▹ e₂ ◃) + move parent +e> ‵▹ ‵ e₁ + e₂ ◃
 
-    AEMIfChild1  : ∀ {e₁ e₂ e₃}
-                 → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 1) +e> (‵ ‵▹ e₁ ◃ ∙₁ e₂ ∙ e₃)
-    AEMIfChild2  : ∀ {e₁ e₂ e₃}
-                 → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 2) +e> (‵ e₁ ∙₂ ‵▹ e₂ ◃ ∙ e₃)
-    AEMIfChild3  : ∀ {e₁ e₂ e₃}
-                 → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 3) +e> (‵ e₁ ∙₃ e₂ ∙ ‵▹ e₃ ◃)
-    AEMIfParent1 : ∀ {e₁ e₂ e₃}
-                 → (‵ ‵▹ e₁ ◃ ∙₁ e₂ ∙ e₃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃
-    AEMIfParent2 : ∀ {e₁ e₂ e₃}
-                 → (‵ e₁ ∙₂ ‵▹ e₂ ◃ ∙ e₃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃
-    AEMIfParent3 : ∀ {e₁ e₂ e₃}
-                 → (‵ e₁ ∙₃ e₂ ∙ ‵▹ e₃ ◃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃
-
-    AEMPairChild1 : ∀ {e₁ e₂}
-                  → ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ + move (child 1) +e> ‵⟨ ‵▹ e₁ ◃ ,₁ e₂ ⟩
-    AEMPairChild2 : ∀ {e₁ e₂}
-                  → ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ + move (child 2) +e> ‵⟨ e₁ ,₂ ‵▹ e₂ ◃ ⟩
+    AEMIfChild1    : ∀ {e₁ e₂ e₃}
+                   → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 1) +e> (‵ ‵▹ e₁ ◃ ∙₁ e₂ ∙ e₃)
+    AEMIfChild2    : ∀ {e₁ e₂ e₃}
+                   → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 2) +e> (‵ e₁ ∙₂ ‵▹ e₂ ◃ ∙ e₃)
+    AEMIfChild3    : ∀ {e₁ e₂ e₃}
+                   → ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃ + move (child 3) +e> (‵ e₁ ∙₃ e₂ ∙ ‵▹ e₃ ◃)
+    AEMIfParent1   : ∀ {e₁ e₂ e₃}
+                   → (‵ ‵▹ e₁ ◃ ∙₁ e₂ ∙ e₃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃
+    AEMIfParent2   : ∀ {e₁ e₂ e₃}
+                   → (‵ e₁ ∙₂ ‵▹ e₂ ◃ ∙ e₃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃
+    AEMIfParent3   : ∀ {e₁ e₂ e₃}
+                   → (‵ e₁ ∙₃ e₂ ∙ ‵▹ e₃ ◃) + move parent +e> ‵▹ ‵ e₁ ∙ e₂ ∙ e₃ ◃
+
+    AEMPairChild1  : ∀ {e₁ e₂}
+                   → ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ + move (child 1) +e> ‵⟨ ‵▹ e₁ ◃ ,₁ e₂ ⟩
+    AEMPairChild2  : ∀ {e₁ e₂}
+                   → ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃ + move (child 2) +e> ‵⟨ e₁ ,₂ ‵▹ e₂ ◃ ⟩
     AEMPairParent1 : ∀ {e₁ e₂}
-                  → ‵⟨ ‵▹ e₁ ◃ ,₁ e₂ ⟩ + move parent +e> ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃
+                   → ‵⟨ ‵▹ e₁ ◃ ,₁ e₂ ⟩ + move parent +e> ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃
     AEMPairParent2 : ∀ {e₁ e₂}
-                  → ‵⟨ e₁ ,₂ ‵▹ e₂ ◃ ⟩ + move parent +e> ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃
+                   → ‵⟨ e₁ ,₂ ‵▹ e₂ ◃ ⟩ + move parent +e> ‵▹ ‵⟨ e₁ , e₂ ⟩ ◃
 
-    AEMProjLChild : ∀ {e}
-                  → ‵▹ ‵π₁ e ◃ + move (child 1) +e> (‵π₁ ‵▹ e ◃)
+    AEMProjLChild  : ∀ {e}
+                   → ‵▹ ‵π₁ e ◃ + move (child 1) +e> (‵π₁ ‵▹ e ◃)
     AEMProjLParent : ∀ {e}
-                  → (‵π₁ ‵▹ e ◃) + move parent +e> ‵▹ ‵π₁ e ◃
-    AEMProjRChild : ∀ {e}
-                  → ‵▹ ‵π₂ e ◃ + move (child 1) +e> (‵π₂ ‵▹ e ◃)
+                   → (‵π₁ ‵▹ e ◃) + move parent +e> ‵▹ ‵π₁ e ◃
+    AEMProjRChild  : ∀ {e}
+                   → ‵▹ ‵π₂ e ◃ + move (child 1) +e> (‵π₂ ‵▹ e ◃)
     AEMProjRParent : ∀ {e}
-                  → (‵π₂ ‵▹ e ◃) + move parent +e> ‵▹ ‵π₂ e ◃
+                   → (‵π₂ ‵▹ e ◃) + move parent +e> ‵▹ ‵π₂ e ◃
 
     -- deletion
     AEDel : ∀ {e u}

diff --git a/hazelnut/untyped/constructability.agda b/hazelnut/untyped/constructability.agda
@@ -9,9 +9,9 @@ open import hazelnut.untyped.erasure
 module hazelnut.untyped.constructability where
   -- constructability of types
   constructability-τ : (τ : Typ) → ∃[ ᾱ ] ▹ unknown ◃ + ᾱ +τ>* ▹ τ ◃
-  constructability-τ num = ⟨ ∣[ construct tnum ] , ATITyp ATConNum ATIRefl ⟩
-  constructability-τ bool = ⟨ ∣[ construct tbool ] , ATITyp ATConBool ATIRefl ⟩
-  constructability-τ unknown = ⟨ [] , ATIRefl ⟩
+  constructability-τ num     = ⟨ ∣[ construct tnum ]  , ATITyp ATConNum ATIRefl  ⟩
+  constructability-τ bool    = ⟨ ∣[ construct tbool ] , ATITyp ATConBool ATIRefl ⟩
+  constructability-τ unknown = ⟨ []                   , ATIRefl                  ⟩
   constructability-τ (τ₁ -→ τ₂)
     with ⟨ ᾱ₁ , +>*τ₁ ⟩ ← constructability-τ τ₁
        | ⟨ ᾱ₂ , +>*τ₂ ⟩ ← constructability-τ τ₂
@@ -28,8 +28,8 @@ module hazelnut.untyped.constructability where
 
   -- constructability of expressions
   constructability-e : ∀ {u} → (e : UExp) → ∃[ ᾱ ] ‵▹ ‵⦇-⦈^ u ◃ + ᾱ +e>* ‵▹ e ◃
-  constructability-e (‵⦇-⦈^ u) = ⟨ ∣[ del _ ] , AEIExp AEDel AEIRefl ⟩
-  constructability-e (‵ x) = ⟨ ∣[ construct (var x) ] , AEIExp AEConVar AEIRefl ⟩
+  constructability-e (‵⦇-⦈^ u) = ⟨ ∣[ del _ ]             , AEIExp AEDel AEIRefl    ⟩
+  constructability-e (‵ x)     = ⟨ ∣[ construct (var x) ] , AEIExp AEConVar AEIRefl ⟩
   constructability-e (‵λ x ∶ τ ∙ e)
     with ⟨ ᾱ₁ , +>*e ⟩ ← constructability-e e
        | ⟨ ᾱ₂ , +>*τ ⟩ ← constructability-τ τ

diff --git a/hazelnut/untyped/determinism.agda b/hazelnut/untyped/determinism.agda
@@ -29,19 +29,19 @@ module hazelnut.untyped.determinism where
   determinism-τ ATConBool           ATConBool      = refl
   determinism-τ (ATZipArr1 ())      ATMArrParent1
   determinism-τ (ATZipArr1 τ^+>τ^′) (ATZipArr1 τ^+>τ^″)
-    rewrite determinism-τ τ^+>τ^′ τ^+>τ^″        = refl
+    rewrite determinism-τ τ^+>τ^′ τ^+>τ^″          = refl
   determinism-τ (ATZipArr2 τ^+>τ^′) (ATZipArr2 τ^+>τ^″)
-    rewrite determinism-τ τ^+>τ^′ τ^+>τ^″        = refl
+    rewrite determinism-τ τ^+>τ^′ τ^+>τ^″          = refl
   determinism-τ (ATZipProd1 τ^+>τ^′) (ATZipProd1 τ^+>τ^″)
-    rewrite determinism-τ τ^+>τ^′ τ^+>τ^″        = refl
+    rewrite determinism-τ τ^+>τ^′ τ^+>τ^″          = refl
   determinism-τ (ATZipProd2 τ^+>τ^′) (ATZipProd2 τ^+>τ^″)
-    rewrite determinism-τ τ^+>τ^′ τ^+>τ^″        = refl
+    rewrite determinism-τ τ^+>τ^′ τ^+>τ^″          = refl
 
   determinism*-τ : ∀ {τ^ τ^′ τ^″ ᾱ} → τ^ + ᾱ +τ>* τ^′ → τ^ + ᾱ +τ>* τ^″ → τ^′ ≡ τ^″
   determinism*-τ ATIRefl                     ATIRefl = refl
   determinism*-τ (ATITyp τ₁^+>τ₂^ τ₂^+>*τ₃^) (ATITyp τ₁^+>τ₂^′ τ₂^+>*τ₃^′)
     rewrite determinism-τ τ₁^+>τ₂^ τ₁^+>τ₂^′
-    rewrite determinism*-τ τ₂^+>*τ₃^ τ₂^+>*τ₃^′    = refl
+    rewrite determinism*-τ τ₂^+>*τ₃^ τ₂^+>*τ₃^′      = refl
 
   determinism-e : ∀ {ê ê′ ê″ α} → ê + α +e> ê′ → ê + α +e> ê″ → ê′ ≡ ê″
   determinism-e AEMLamChild1        AEMLamChild1   = refl
@@ -94,38 +94,38 @@ module hazelnut.untyped.determinism where
   determinism-e AEConProjL          AEConProjL     = refl
   determinism-e AEConProjR          AEConProjR     = refl
   determinism-e (AEZipLam1 τ^+>τ^′) (AEZipLam1 τ^+>τ^″)
-    rewrite determinism-τ τ^+>τ^′ τ^+>τ^″        = refl
+    rewrite determinism-τ τ^+>τ^′ τ^+>τ^″          = refl
   determinism-e (AEZipLam2 ê+>ê′)   (AEZipLam2 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipAp1 ê+>ê′)    (AEZipAp1 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipAp2 ê+>ê′)    (AEZipAp2 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipLet1 ê+>ê′)   (AEZipLet1 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipLet2 ê+>ê′)   (AEZipLet2 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipPlus1 ê+>ê′)  (AEZipPlus1 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipPlus2 ê+>ê′)  (AEZipPlus2 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipIf1 ê+>ê′)    (AEZipIf1 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipIf2 ê+>ê′)    (AEZipIf2 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipIf3 ê+>ê′)    (AEZipIf3 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipPair1 ê+>ê′)  (AEZipPair1 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipPair2 ê+>ê′)  (AEZipPair2 ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipProjL ê+>ê′)  (AEZipProjL ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
   determinism-e (AEZipProjR ê+>ê′)  (AEZipProjR ê+>ê″)
-    rewrite determinism-e ê+>ê′ ê+>ê″            = refl
+    rewrite determinism-e ê+>ê′ ê+>ê″              = refl
 
   determinism*-e : ∀ {ê ê′ ê″ ᾱ} → ê + ᾱ +e>* ê′ → ê + ᾱ +e>* ê″ → ê′ ≡ ê″
   determinism*-e AEIRefl                 AEIRefl = refl
   determinism*-e (AEIExp ê₁+>ê₂ ê₂+>*ê₃) (AEIExp ê₁+>ê₂′ ê₂+>*ê₃′)
     rewrite determinism-e ê₁+>ê₂ ê₁+>ê₂′
-    rewrite determinism*-e ê₂+>*ê₃ ê₂+>*ê₃′    = refl
+    rewrite determinism*-e ê₂+>*ê₃ ê₂+>*ê₃′      = refl
diff --git a/hazelnut/untyped/erasure.agda b/hazelnut/untyped/erasure.agda
@@ -6,9 +6,9 @@ open import hazelnut.untyped.zexp
 module hazelnut.untyped.erasure where
   -- judgmental cursor erasure
   data erase-τ : (τ^ : ZTyp) → (τ : Typ) → Set where
-    ETTop  : ∀ {τ} → erase-τ (▹ τ ◃) τ
-    ETArr1 : ∀ {τ₁^ τ₂ τ₁} → (τ₁^◇ : erase-τ τ₁^ τ₁) → erase-τ (τ₁^ -→₁ τ₂) (τ₁ -→ τ₂)
-    ETArr2 : ∀ {τ₁ τ₂^ τ₂} → (τ₂^◇ : erase-τ τ₂^ τ₂) → erase-τ (τ₁ -→₂ τ₂^) (τ₁ -→ τ₂)
+    ETTop   : ∀ {τ} → erase-τ (▹ τ ◃) τ
+    ETArr1  : ∀ {τ₁^ τ₂ τ₁} → (τ₁^◇ : erase-τ τ₁^ τ₁) → erase-τ (τ₁^ -→₁ τ₂) (τ₁ -→ τ₂)
+    ETArr2  : ∀ {τ₁ τ₂^ τ₂} → (τ₂^◇ : erase-τ τ₂^ τ₂) → erase-τ (τ₁ -→₂ τ₂^) (τ₁ -→ τ₂)
     ETProd1 : ∀ {τ₁^ τ₂ τ₁} → (τ₁^◇ : erase-τ τ₁^ τ₁) → erase-τ (τ₁^ -×₁ τ₂) (τ₁ -× τ₂)
     ETProd2 : ∀ {τ₁ τ₂^ τ₂} → (τ₂^◇ : erase-τ τ₂^ τ₂) → erase-τ (τ₁ -×₂ τ₂^) (τ₁ -× τ₂)
 
@@ -104,33 +104,33 @@ module hazelnut.untyped.erasure where
   erase-e→◇ (EELam1 τ^◇)
     rewrite erase-τ→◇ τ^◇ = refl
   erase-e→◇ (EELam2 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEAp1 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEAp2 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EELet1 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EELet2 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEPlus1 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEPlus2 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEIf1 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEIf2 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEIf3 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEPair1 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEPair2 ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEProjL ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
   erase-e→◇ (EEProjR ê◇)
-    rewrite erase-e→◇ ê◇ = refl
+    rewrite erase-e→◇ ê◇  = refl
 
   -- convert functional cursor erasure to judgmental cursor erasure
   ◇τ→erase : ∀ {τ^ τ} → τ^ ◇τ ≡ τ → erase-τ τ^ τ