From a27c41c5d137a4e316b48adf8798f61527376e82 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Wed, 29 Jan 2025 12:19:45 -0500
Subject: [PATCH] Add lemmas that bad forms are impossible

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

diff --git a/theories/fp_red.v b/theories/fp_red.v
index dbe7312..6fe95a1 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -147,6 +147,26 @@ with TRedSN {n} : PTm n -> PTm n -> Prop :=
   TRedSN a b ->
   TRedSN (PProj p a) (PProj p b).
 
+Lemma PProjAbs_imp n p (a : PTm (S n)) :
+  ~ SN (PProj p (PAbs a)).
+Proof.
+  move E : (PProj p (PAbs a)) => u hu.
+  move : p a E.
+  elim : n u / hu=>//=.
+  hauto lq:on inv:SNe.
+  hauto lq:on inv:TRedSN.
+Qed.
+
+Lemma PProjPair_imp n (a b0 b1 : PTm n ) :
+  ~ SN (PApp (PPair b0 b1) a).
+Proof.
+  move E : (PApp (PPair b0 b1) a) => u hu.
+  move : a b0 b1 E.
+  elim : n u / hu=>//=.
+  hauto lq:on inv:SNe.
+  hauto lq:on inv:TRedSN.
+Qed.
+
 Scheme sne_ind := Induction for SNe Sort Prop
   with sn_ind := Induction for SN Sort Prop
   with sred_ind := Induction for TRedSN Sort Prop.
@@ -531,6 +551,8 @@ Proof.
   - scongruence b:on.
 Qed.
 
+
+
 Lemma η_nf'' n (a b : PTm n) : ERed'.R a b -> nf b -> nf a \/ rtc RRed.R a b.
 Proof.
   move => h.