diff --git a/progs/verif_io.v b/progs/verif_io.v
index a28445ba1..1eabbba6f 100644
--- a/progs/verif_io.v
+++ b/progs/verif_io.v
@@ -130,6 +130,24 @@ Qed.
 
 Opaque Nat.div Nat.modulo.
 
+Import Program.Wf. 
+  Program Lemma fix_sub_eq_ext :
+   (* need to copy this from Coq standard library because it moved from
+    one location to another between Coq 8.20 and Coq 8.21 *)
+    forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Type)
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (proj1_sig y)) -> P x),
+      forall x : A,
+        Fix_sub A R Rwf P F_sub x =
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (proj1_sig y)).
+  Proof.
+    intros A R Rwf P F_sub x; apply Fix_eq ; auto.
+    intros ? f g H.
+    assert(f = g) as H0.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
+  Qed.
+
 Lemma intr_eq : forall n, intr n =
   match n <=? 0 with
   | true => []
@@ -138,7 +156,7 @@ Lemma intr_eq : forall n, intr n =
 Proof.
   intros.
   unfold intr at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold intr.
+  rewrite fix_sub_eq_ext; simpl; fold intr.
   destruct n; reflexivity.
 Qed.
 
@@ -230,7 +248,7 @@ Lemma chars_of_Z_eq : forall n, chars_of_Z n =
 Proof.
   intros.
   unfold chars_of_Z at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
+  rewrite fix_sub_eq_ext; simpl; fold chars_of_Z.
   destruct (_ <=? _); reflexivity.
 Qed.
 
diff --git a/progs/verif_io_mem.v b/progs/verif_io_mem.v
index e64dfba38..7650e9ebd 100644
--- a/progs/verif_io_mem.v
+++ b/progs/verif_io_mem.v
@@ -116,6 +116,24 @@ Qed.
 
 Opaque Nat.div Nat.modulo.*)
 
+Import Program.Wf. 
+  Program Lemma fix_sub_eq_ext :
+   (* need to copy this from Coq standard library because it moved from
+    one location to another between Coq 8.20 and Coq 8.21 *)
+    forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Type)
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (proj1_sig y)) -> P x),
+      forall x : A,
+        Fix_sub A R Rwf P F_sub x =
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (proj1_sig y)).
+  Proof.
+    intros A R Rwf P F_sub x; apply Fix_eq ; auto.
+    intros ? f g H.
+    assert(f = g) as H0.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
+  Qed.
+
 Lemma intr_eq : forall n, intr n =
   match n <=? 0 with
   | true => []
@@ -124,7 +142,7 @@ Lemma intr_eq : forall n, intr n =
 Proof.
   intros.
   unfold intr at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold intr.
+  rewrite fix_sub_eq_ext; simpl; fold intr.
   destruct n; reflexivity.
 Qed.
 
@@ -226,7 +244,7 @@ Lemma chars_of_Z_eq : forall n, chars_of_Z n =
 Proof.
   intros.
   unfold chars_of_Z at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
+  rewrite fix_sub_eq_ext; simpl; fold chars_of_Z.
   destruct (_ <=? _); reflexivity.
 Qed.
 
diff --git a/progs64/verif_io.v b/progs64/verif_io.v
index b24425891..d461b2c94 100644
--- a/progs64/verif_io.v
+++ b/progs64/verif_io.v
@@ -130,6 +130,24 @@ Qed.
 
 Opaque Nat.div Nat.modulo.
 
+Import Program.Wf. 
+  Program Lemma fix_sub_eq_ext :
+   (* need to copy this from Coq standard library because it moved from
+    one location to another between Coq 8.20 and Coq 8.21 *)
+    forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Type)
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (proj1_sig y)) -> P x),
+      forall x : A,
+        Fix_sub A R Rwf P F_sub x =
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (proj1_sig y)).
+  Proof.
+    intros A R Rwf P F_sub x; apply Fix_eq ; auto.
+    intros ? f g H.
+    assert(f = g) as H0.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
+  Qed.
+
 Lemma intr_eq : forall n, intr n =
   match n <=? 0 with
   | true => []
@@ -138,7 +156,7 @@ Lemma intr_eq : forall n, intr n =
 Proof.
   intros.
   unfold intr at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold intr.
+  rewrite fix_sub_eq_ext; simpl; fold intr.
   destruct n; reflexivity.
 Qed.
 
@@ -230,7 +248,7 @@ Lemma chars_of_Z_eq : forall n, chars_of_Z n =
 Proof.
   intros.
   unfold chars_of_Z at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
+  rewrite fix_sub_eq_ext; simpl; fold chars_of_Z.
   destruct (_ <=? _); reflexivity.
 Qed.
 
diff --git a/progs64/verif_io_mem.v b/progs64/verif_io_mem.v
index 34b16cbc8..0068890ec 100644
--- a/progs64/verif_io_mem.v
+++ b/progs64/verif_io_mem.v
@@ -116,6 +116,24 @@ Qed.
 
 Opaque Nat.div Nat.modulo.*)
 
+Import Program.Wf. 
+  Program Lemma fix_sub_eq_ext :
+   (* need to copy this from Coq standard library because it moved from
+    one location to another between Coq 8.20 and Coq 8.21 *)
+    forall (A : Type) (R : A -> A -> Prop) (Rwf : well_founded R)
+      (P : A -> Type)
+      (F_sub : forall x : A, (forall y:{y : A | R y x}, P (proj1_sig y)) -> P x),
+      forall x : A,
+        Fix_sub A R Rwf P F_sub x =
+          F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (proj1_sig y)).
+  Proof.
+    intros A R Rwf P F_sub x; apply Fix_eq ; auto.
+    intros ? f g H.
+    assert(f = g) as H0.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
+  Qed.
+
 Lemma intr_eq : forall n, intr n =
   match n <=? 0 with
   | true => []
@@ -124,7 +142,7 @@ Lemma intr_eq : forall n, intr n =
 Proof.
   intros.
   unfold intr at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold intr.
+  rewrite fix_sub_eq_ext; simpl; fold intr.
   destruct n; reflexivity.
 Qed.
 
@@ -226,7 +244,7 @@ Lemma chars_of_Z_eq : forall n, chars_of_Z n =
 Proof.
   intros.
   unfold chars_of_Z at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
+  rewrite fix_sub_eq_ext; simpl; fold chars_of_Z.
   destruct (_ <=? _); reflexivity.
 Qed.