diff --git a/ahmed/day1.agda b/ahmed/day1.agda
index 3495fd2..4a3e281 100644
--- a/ahmed/day1.agda
+++ b/ahmed/day1.agda
@@ -69,27 +69,24 @@ data steps : ℕ → term → term → Set where
   zero : ∀ {e} → steps zero e e
   suc : ∀ {e e' e''} → (n : ℕ) → step e e' → steps n e' e'' → steps (suc n) e e''
 
-data well-typed : ctx → term → type → Set where
-  type-`true : ∀ {ctx} → well-typed ctx `true bool
-  type-`false : ∀ {ctx} → well-typed ctx `false bool
+data _⊢_∶_ : ctx → term → type → Set where
+  type-`true : ∀ {ctx} → ctx ⊢ `true ∶ bool
+  type-`false : ∀ {ctx} → ctx ⊢ `false ∶ bool
   type-`ifthenelse : ∀ {ctx e e₁ e₂ τ}
-    → well-typed ctx e bool
-    → well-typed ctx e₁ τ
-    → well-typed ctx e₂ τ
-    → well-typed ctx (`if e then e₁ else e₂) τ
+    → ctx ⊢ e ∶ bool
+    → ctx ⊢ e₁ ∶ τ
+    → ctx ⊢ e₂ ∶ τ
+    → ctx ⊢ (`if e then e₁ else e₂) ∶ τ
   type-`x : ∀ {ctx x}
     → (p : Is-just (lookup ctx x))
-    → well-typed ctx (` x) (to-witness p)
+    → ctx ⊢ (` x) ∶ (to-witness p)
   type-`λ : ∀ {ctx τ τ₂ e}
-    → well-typed (cons ctx τ) e τ₂
-    → well-typed ctx (`λ[ τ ] e) (τ -→ τ₂)
+    → (cons ctx τ) ⊢ e ∶ τ₂
+    → ctx ⊢ (`λ[ τ ] e) ∶ (τ -→ τ₂)
   type-∙ : ∀ {ctx τ₁ τ₂ e₁ e₂}
-    → well-typed ctx e₁ (τ₁ -→ τ₂)
-    → well-typed ctx e₂ τ₂
-    → well-typed ctx (e₁ ∙ e₂) τ₂
-
-_⊢_∶_ : (Γ : ctx) → (e : term) → (τ : type) → Set
-Γ ⊢ e ∶ τ = (well-typed Γ e τ) × (∀ {n} → (e' : term) → steps n e e' → value-rel τ e' ⊎ ∃ λ e'' → step e' e'')
+    → ctx ⊢ e₁ ∶ (τ₁ -→ τ₂)
+    → ctx ⊢ e₂ ∶ τ₂
+    → ctx ⊢ (e₁ ∙ e₂) ∶ τ₂
 
 irreducible : term → Set
 irreducible e = ¬ (∃ λ e' → step e e')
@@ -99,11 +96,14 @@ data term-relation : type → term → Set where
     → (∀ {n} → (e' : term) → steps n e e' → irreducible e' → value-rel τ e')
     → term-relation τ e
 
+type-sound : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Set
+type-sound {Γ} {e} {τ} s = ∀ {n} → (e' : term) → steps n e e' → value-rel τ e' ⊎ ∃ λ e'' → step e' e''
+
 _⊨_∶_ : (Γ : ctx) → (e : term) → (τ : type) → Set
 _⊨_∶_ Γ e τ = (γ : sub) → (good-subst Γ γ) → term-relation τ e
 
-fundamental : ∀ {Γ e τ} → Γ ⊢ e ∶ τ → Γ ⊨ e ∶ τ
-fundamental {Γ} {e} {τ} type-sound γ good-sub = e-term f
+fundamental : ∀ {Γ e τ} → (well-typed : Γ ⊢ e ∶ τ) → type-sound well-typed → Γ ⊨ e ∶ τ
+fundamental {Γ} {e} {τ} well-typed type-sound γ good-sub = e-term f
   where
     f : {n : ℕ} (e' : term) → steps n e e' → irreducible e' → value-rel τ e'
-    f e' steps irred = [ id , (λ exists → ⊥-elim (irred exists)) ] (snd type-sound e' steps)
\ No newline at end of file
+    f e' steps irred = [ id , (λ exists → ⊥-elim (irred exists)) ] (type-sound e' steps)
\ No newline at end of file