From d925a8bcaa5c51d915600b3599c741690d0ad886 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Thu, 30 Jan 2025 20:23:57 -0500
Subject: [PATCH] Minor cleanup

---
 theories/fp_red.v | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index a53a692..abc951e 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -144,16 +144,6 @@ with TRedSN {n} : PTm n -> PTm n -> Prop :=
 
 Derive Dependent Inversion tred_inv with (forall n (a b : PTm n), TRedSN a b) Sort Prop.
 
-Inductive SNe' {n} : PTm n -> Prop :=
-| N_Var' i :
-  SNe' (VarPTm i)
-| N_App' a b :
-  SNe a ->
-  SNe' (PApp a b)
-| N_Proj' p a :
-  SNe a ->
-  SNe' (PProj p a).
-
 Lemma PProjAbs_imp n p (a : PTm (S n)) :
   ~ SN (PProj p (PAbs a)).
 Proof.