theories/fp_red.v

@@ -1707,6 +1707,15 @@ Module REReds.
     elim : u C / hu; sauto lq:on rew:off.
   Qed.
 
+  Lemma univ_inv n i C :
+    rtc (@RERed.R n) (PUniv i) C  ->
+    C = PUniv i.
+  Proof.
+    move E : (PUniv i) => u hu.
+    move : i E. elim : u C / hu=>//=.
+    hauto lq:on rew:off ctrs:rtc inv:RERed.R.
+  Qed.
+
 End REReds.
 
 Module LoRed.
@@ -2139,6 +2148,12 @@ Module DJoin.
     hauto lq:on rew:off use:REReds.bind_inv.
   Qed.
 
+  Lemma univ_inj n i j :
+    @R n (PUniv i) (PUniv j)  -> i = j.
+  Proof.
+    sauto lq:on rew:off use:REReds.univ_inv.
+  Qed.
+
   Lemma FromRRed0 n (a b : PTm n) :
     RRed.R a b -> R a b.
   Proof.
@@ -2151,4 +2166,6 @@ Module DJoin.
     hauto lq:on ctrs:rtc use:RERed.FromBeta unfold:R.
   Qed.
 
+
+
 End DJoin.

theories/logrel.v

@@ -370,7 +370,7 @@ Proof.
     hauto l:on use: DJoin.sne_univ_noconf, DJoin.bind_univ_noconf, DJoin.symmetric.
     case : H h1 h => //=.
     move => j' hPB h _.
-    have {}h : j' = j by admit. subst.
+    have {}h : j' = j by hauto lq:on use: DJoin.univ_inj. subst.
     hauto lq:on use:InterpUniv_Univ_inv.
   - move => i A A0 PA hr hPA ihPA B PB hPB hAB.
     have /DJoin.symmetric ? : DJoin.R A A0 by hauto lq:on rew:off ctrs:rtc use:DJoin.FromRedSNs.
@@ -378,4 +378,4 @@ Proof.
     have ? : SN A by eauto using N_Exp.
     have : DJoin.R A0 B by eauto using DJoin.transitive.
     eauto.
-Admitted.
+Qed.