From 7ffb8a912dca11270e4cf741902136d5e1056b70 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sat, 4 Jan 2025 01:48:31 -0500
Subject: [PATCH] Add some todos

---
 theories/fp_red.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index 16922c9..c9bcec2 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -1064,7 +1064,10 @@ Definition prov_univ {n} i0 (a : Tm n) :=
 (* Can consider combine prov and provU *)
 #[tactic="prov_tac"]Equations prov {n} (h : Tm n) (a : Tm n) : Prop by wf (depth_tm a) lt :=
   prov h (TBind p0 A0 B0) := prov_bind p0 A0 B0 h;
+ (* TODOS *)
  (* Try forall b, prov h (a {b /x})? *)
+ (* Replace the parallel red from I_Red with Strong normalization *)
+ (* Prove the uniqueness of eta normal form for terms in beta normal form *)
   prov h (Abs a) := prov (ren_Tm shift h) a;
   prov h (App a b) := prov h a;
   prov h (Pair a b) := prov h a /\ prov h b;