From e3a6e5f16e91e4b79a52bf11301db02211c74528 Mon Sep 17 00:00:00 2001
From: Li-yao Xia
Date: Thu, 12 Nov 2020 23:35:45 -0500
Subject: Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-free

---
 theories/Program/Wf.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 50351d6a14..688db8b812 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -12,8 +12,6 @@
 
 Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
-Require Import ProofIrrelevance.
-Require Import FunctionalExtensionality.
 
 Local Open Scope program_scope.
 
@@ -51,7 +49,7 @@ Section Well_founded.
   Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s.
   Proof.
     intro x; induction (Rwf x); intros.
-    rewrite (proof_irrelevance (Acc R x) r s) ; auto.
+    rewrite <- 2 Fix_F_eq; intros. apply F_ext; intros []; auto.
   Qed.
 
   Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun y:{ y:A | R y x} => Fix_sub (proj1_sig y)).
@@ -226,6 +224,7 @@ Ltac fold_sub f :=
 
 (** This module provides the fixpoint equation provided one assumes
    functional extensionality. *)
+Require Import FunctionalExtensionality.
 
 Module WfExtensionality.
 
-- 
cgit v1.2.3