From 162db5296fa7c6785b44e7d02298d135665ce115 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Sat, 4 Jan 2025 01:31:02 -0500
Subject: [PATCH] Stuck

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

diff --git a/theories/fp_red.v b/theories/fp_red.v
index ff65521..f48de65 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -1132,6 +1132,31 @@ Qed.
 Lemma prov_antiren n m (ξ : fin n -> fin m) h a:
   prov (ren_Tm ξ h) a -> exists a', ren_Tm ξ a' = a /\ prov h a'.
 Proof.
+  move E : (ren_Tm ξ h) => H.
+  move : ξ H E.
+  elim : m / a => m.
+  - move => i ξ H ?. subst. simp prov.
+    case : h => //=.
+    move => j [?]. subst.
+    exists (VarTm j). firstorder.
+  - move => a iha ξ ? ?. subst.
+    simp prov.
+    asimpl.
+    move => {}/iha iha.
+    specialize iha with (1 := eq_refl).
+    move : iha => [a' [h1 h2]]. subst.
+    exists (Abs (ren_Tm shift a')).
+    split. by asimpl.
+    simp prov. hauto lq:on use:prov_ren.
+  - move => a iha b ihb ξ ? ?. subst.
+    simp prov.
+    move /iha. move/(_ ξ eq_refl) => [a' [? ?]] {iha ihb}. subst.
+    (* Doesn't hold *)
+    have : exists b', ren_Tm ξ b' = b by admit.
+    move => [b' ?]. subst.
+    exists (App a' b').
+    split => //=.
+    simp prov.
 Admitted.
 
 (* Lemma ren_hfb {n m} (ξ : fin n -> fin m) u  : hfb (ren_Tm ξ u) = hfb u. *)