Now proving CT-VarW is easy

0xd34df00d · May 19, 2021 · 28fe5e2 · 28fe5e2
1 parent 954b82d
commit 28fe5e2
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/agda/Core/Syntax/Derived/Typing.agda b/agda/Core/Syntax/Derived/Typing.agda
@@ -72,7 +72,8 @@ CT-VarW : Γ ⊢ τ ⦂ CSort s
 CT-VarW δ (∈-zero refl) with head-well-formed δ
 ... | ⟨ _ , δ' ⟩ = CT-Var δ'
 CT-VarW δ (∈-suc refl ∈) with head-well-formed δ
-... | ⟨ _ , δ' ⟩ = CT-Weaken (CT-VarW (unweaken' δ) ∈) δ'
+... | ⟨ _ , δ' ⟩ with τ∈Γ-wf δ' ∈
+...   | ⟨ _ , δ'' ⟩ = CT-Weaken (CT-VarW δ'' ∈) δ'
 
 ⇒'-well-typed : Γ ⊢ τ₁ ⦂ CSort s₁
               → Γ ⊢ τ₂ ⦂ CSort s₂