Wf.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Reformulation of the Wf module using subsets where possible, providing the support for Program's treatment of well-founded definitions.

Require Import Coq.Init.Wf.
Require Import Coq.Program.Utils.
Require Import ProofIrrelevance.
Require Import FunctionalExtensionality.

Local Open Scope program_scope.

Section Well_founded.
  Variable A : Type.
  Variable R : A -> A -> Prop.
  Hypothesis Rwf : well_founded R.

  Variable P : A -> Type.

  Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.

  Fixpoint Fix_F_sub (x : A) (r : Acc R x) : P x :=
    F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y)
      (Acc_inv r (proj2_sig y))).

  Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).

  Register Fix_sub as program.wf.fix_sub.

  (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *)
  (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *)

  Hypothesis F_ext :
    forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
      (forall y:{y : A | R y x}, f y = g y) -> F_sub x f = F_sub x g.

  Lemma Fix_F_eq :
    forall (x:A) (r:Acc R x),
      F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.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 (` y)) -> P x
F_ext:forall (x : A)
  (f g : forall y : {y : A | R y x}, P (` y)),
(forall y : {y : A | R y x}, f y = g y) ->
F_sub x f = F_sub x g
forall (x : A) (r : Acc R x),
F_sub x
  (fun y : {y : A | R y x} =>
   Fix_F_sub (` y) (Acc_inv r (proj2_sig y))) =
Fix_F_sub x r
  Proof.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 (` y)) -> P x
F_ext:forall (x : A)
  (f g : forall y : {y : A | R y x}, P (` y)),
(forall y : {y : A | R y x}, f y = g y) ->
F_sub x f = F_sub x g
forall (x : A) (r : Acc R x),
F_sub x
  (fun y : {y : A | R y x} =>
   Fix_F_sub (` y) (Acc_inv r (proj2_sig y))) =
Fix_F_sub x r
    destruct r using Acc_inv_dep; auto.
  Qed.

  Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s.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 (` y)) -> P x
F_ext:forall (x : A)
  (f g : forall y : {y : A | R y x}, P (` y)),
(forall y : {y : A | R y x}, f y = g y) ->
F_sub x f = F_sub x g
forall (x : A) (r s : Acc R x),
Fix_F_sub x r = Fix_F_sub x s
  Proof.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 (` y)) -> P x
F_ext:forall (x : A)
  (f g : forall y : {y : A | R y x}, P (` y)),
(forall y : {y : A | R y x}, f y = g y) ->
F_sub x f = F_sub x g
forall (x : A) (r s : Acc R x),
Fix_F_sub x r = Fix_F_sub x s
    intro x; induction (Rwf x); intros.A:Type
R:A -> A -> Prop
Rwf:well_founded R
P:A -> Type
F_sub:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
F_ext:forall (x0 : A)
  (f g : forall y : {y : A | R y x0}, P (` y)),
(forall y : {y : A | R y x0}, f y = g y) ->
F_sub x0 f = F_sub x0 g
x:A
H:forall y : A, R y x -> Acc R y
H0:forall y : A,
R y x ->
forall r0 s0 : Acc R y,
Fix_F_sub y r0 = Fix_F_sub y s0
r, s:Acc R x
Fix_F_sub x r = Fix_F_sub x s
    rewrite (proof_irrelevance (Acc R x) r s) ; 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)).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 (` y)) -> P x
F_ext:forall (x : A)
  (f g : forall y : {y : A | R y x}, P (` y)),
(forall y : {y : A | R y x}, f y = g y) ->
F_sub x f = F_sub x g
forall x : A,
Fix_sub x =
F_sub x (fun y : {y : A | R y x} => Fix_sub (` y))
  Proof.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 (` y)) -> P x
F_ext:forall (x : A)
  (f g : forall y : {y : A | R y x}, P (` y)),
(forall y : {y : A | R y x}, f y = g y) ->
F_sub x f = F_sub x g
forall x : A,
Fix_sub x =
F_sub x (fun y : {y : A | R y x} => Fix_sub (` y))
    intro x; unfold Fix_sub.A:Type
R:A -> A -> Prop
Rwf:well_founded R
P:A -> Type
F_sub:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
F_ext:forall (x0 : A)
  (f g : forall y : {y : A | R y x0}, P (` y)),
(forall y : {y : A | R y x0}, f y = g y) ->
F_sub x0 f = F_sub x0 g
x:A
Fix_F_sub x (Rwf x) =
F_sub x
  (fun y : {y : A | R y x} =>
   Fix_F_sub (` y) (Rwf (` y)))
    rewrite <- (Fix_F_eq ).A:Type
R:A -> A -> Prop
Rwf:well_founded R
P:A -> Type
F_sub:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
F_ext:forall (x0 : A)
  (f g : forall y : {y : A | R y x0}, P (` y)),
(forall y : {y : A | R y x0}, f y = g y) ->
F_sub x0 f = F_sub x0 g
x:A
F_sub x
  (fun y : {y : A | R y x} =>
   Fix_F_sub (` y) (Acc_inv (Rwf x) (proj2_sig y))) =
F_sub x
  (fun y : {y : A | R y x} =>
   Fix_F_sub (` y) (Rwf (` y)))
    apply F_ext; intros.A:Type
R:A -> A -> Prop
Rwf:well_founded R
P:A -> Type
F_sub:forall x0 : A,
(forall y0 : {y0 : A | R y0 x0}, P (` y0)) ->
P x0
F_ext:forall (x0 : A)
  (f
   g : forall y0 : {y0 : A | R y0 x0},
       P (` y0)),
(forall y0 : {y0 : A | R y0 x0}, f y0 = g y0) ->
F_sub x0 f = F_sub x0 g
x:A
y:{y0 : A | R y0 x}
Fix_F_sub (` y) (Acc_inv (Rwf x) (proj2_sig y)) =
Fix_F_sub (` y) (Rwf (` y))
    apply Fix_F_inv.
  Qed.

  Lemma fix_sub_eq :
    forall x : A,
      Fix_sub x =
      let f_sub := F_sub in
        f_sub x (fun y: {y : A | R y x} => Fix_sub (`y)).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 (` y)) -> P x
F_ext:forall (x : A)
  (f g : forall y : {y : A | R y x}, P (` y)),
(forall y : {y : A | R y x}, f y = g y) ->
F_sub x f = F_sub x g
forall x : A,
Fix_sub x =
(let f_sub := F_sub in
 f_sub x (fun y : {y : A | R y x} => Fix_sub (` y)))
  Proof.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 (` y)) -> P x
F_ext:forall (x : A)
  (f g : forall y : {y : A | R y x}, P (` y)),
(forall y : {y : A | R y x}, f y = g y) ->
F_sub x f = F_sub x g
forall x : A,
Fix_sub x =
(let f_sub := F_sub in
 f_sub x (fun y : {y : A | R y x} => Fix_sub (` y)))
    exact Fix_eq.
  Qed.

End Well_founded.

Require Coq.extraction.Extraction.
Extraction Inline Fix_F_sub Fix_sub.

Set Implicit Arguments.

Reasoning about well-founded fixpoints on measures.

Section Measure_well_founded.

  (* Measure relations are well-founded if the underlying relation is well-founded. *)

  Variables T M: Type.
  Variable R: M -> M -> Prop.
  Hypothesis wf: well_founded R.
  Variable m: T -> M.

  Definition MR (x y: T): Prop := R (m x) (m y).

  Register MR as program.wf.mr.

  Lemma measure_wf: well_founded MR.T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
well_founded MR
  Proof with auto.T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
well_founded MR
    unfold well_founded.T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
forall a : T, Acc MR a
    cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0).T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
(forall (a : M) (a0 : T), m a0 = a -> Acc MR a0) ->
forall a : T, Acc MR a
T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
forall (a : M) (a0 : T), m a0 = a -> Acc MR a0
    +T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
(forall (a : M) (a0 : T), m a0 = a -> Acc MR a0) ->
forall a : T, Acc MR a intros.T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
H:forall (a0 : M) (a1 : T), m a1 = a0 -> Acc MR a1
a:T
Acc MR a
      apply (H (m a))...
    +T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
forall (a : M) (a0 : T), m a0 = a -> Acc MR a0 apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
forall x : M,
(forall y : M,
 R y x -> forall a : T, m a = y -> Acc MR a) ->
forall a : T, m a = x -> Acc MR a
      intros.T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
x:M
H:forall y : M,
R y x -> forall a0 : T, m a0 = y -> Acc MR a0
a:T
H0:m a = x
Acc MR a
      apply Acc_intro.T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
x:M
H:forall y : M,
R y x -> forall a0 : T, m a0 = y -> Acc MR a0
a:T
H0:m a = x
forall y : T, MR y a -> Acc MR y
      intros.T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
x:M
H:forall y0 : M,
R y0 x -> forall a0 : T, m a0 = y0 -> Acc MR a0
a:T
H0:m a = x
y:T
H1:MR y a
Acc MR y
      unfold MR in H1.T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
x:M
H:forall y0 : M,
R y0 x -> forall a0 : T, m a0 = y0 -> Acc MR a0
a:T
H0:m a = x
y:T
H1:R (m y) (m a)
Acc MR y
      rewrite H0 in H1.T, M:Type
R:M -> M -> Prop
wf:well_founded R
m:T -> M
x:M
H:forall y0 : M,
R y0 x -> forall a0 : T, m a0 = y0 -> Acc MR a0
a:T
H0:m a = x
y:T
H1:R (m y) x
Acc MR y
      apply (H (m y))...
  Defined.

End Measure_well_founded.

Hint Resolve measure_wf : core.

Section Fix_rects.

  Variable A: Type.
  Variable P: A -> Type.
  Variable R : A -> A -> Prop.
  Variable Rwf : well_founded R.
  Variable f: forall (x : A), (forall y: { y: A | R y x }, P (proj1_sig y)) -> P x.

  Lemma F_unfold x r:
    Fix_F_sub A R P f x r =
    f (fun y => Fix_F_sub A R P f (proj1_sig y) (Acc_inv r (proj2_sig y))).A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
x:A
r:Acc R x
Fix_F_sub A R P f x r =
f
  (fun y : {y : A | R y x} =>
   Fix_F_sub A R P f (` y) (Acc_inv r (proj2_sig y)))
  Proof.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
x:A
r:Acc R x
Fix_F_sub A R P f x r =
f
  (fun y : {y : A | R y x} =>
   Fix_F_sub A R P f (` y) (Acc_inv r (proj2_sig y))) intros.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
x:A
r:Acc R x
Fix_F_sub A R P f x r =
f
  (fun y : {y : A | R y x} =>
   Fix_F_sub A R P f (` y) (Acc_inv r (proj2_sig y))) case r; auto. Qed.

  (* Fix_F_sub_rect lets one prove a property of
  functions defined using Fix_F_sub by showing
  that property to be invariant over single application of the
  function body (f in our case). *)

  Lemma Fix_F_sub_rect
    (Q: forall x, P x -> Type)
    (inv: forall x: A,
     (forall (y: A) (H: R y x) (a: Acc R y),
        Q y (Fix_F_sub A R P f y a)) ->
        forall (a: Acc R x),
          Q x (f (fun y: {y: A | R y x} =>
            Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y)))))
    : forall x a, Q _ (Fix_F_sub A R P f x a).A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x : A,
(forall y : {y : A | R y x}, P (` y)) -> P x
Q:forall x : A, P x -> Type
inv:forall x : A,
(forall y : A, R y x -> forall a : Acc R y, Q y (Fix_F_sub A R P f y a)) ->
forall a : Acc R x,
Q x
(f
(fun y : {y : A | R y x} =>
Fix_F_sub A R P f (` y) (Acc_inv a (proj2_sig y))))
forall (x : A) (a : Acc R x),
Q x (Fix_F_sub A R P f x a)
  Proof with auto.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x : A,
(forall y : {y : A | R y x}, P (` y)) -> P x
Q:forall x : A, P x -> Type
inv:forall x : A,
(forall y : A, R y x -> forall a : Acc R y, Q y (Fix_F_sub A R P f y a)) ->
forall a : Acc R x,
Q x
(f
(fun y : {y : A | R y x} =>
Fix_F_sub A R P f (` y) (Acc_inv a (proj2_sig y))))
forall (x : A) (a : Acc R x),
Q x (Fix_F_sub A R P f x a)
    set (R' := fun (x: A) => forall a, Q _ (Fix_F_sub A R P f x a)).A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x : A,
(forall y : {y : A | R y x}, P (` y)) -> P x
Q:forall x : A, P x -> Type
inv:forall x : A,
(forall y : A, R y x -> forall a : Acc R y, Q y (Fix_F_sub A R P f y a)) ->
forall a : Acc R x,
Q x
(f
(fun y : {y : A | R y x} =>
Fix_F_sub A R P f (` y) (Acc_inv a (proj2_sig y))))
R':=fun x : A =>
forall a : Acc R x, Q x (Fix_F_sub A R P f x a):A -> Type
forall (x : A) (a : Acc R x),
Q x (Fix_F_sub A R P f x a)
    cut (forall x, R' x)...A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x : A,
(forall y : {y : A | R y x}, P (` y)) -> P x
Q:forall x : A, P x -> Type
inv:forall x : A,
(forall y : A, R y x -> forall a : Acc R y, Q y (Fix_F_sub A R P f y a)) ->
forall a : Acc R x,
Q x
(f
(fun y : {y : A | R y x} =>
Fix_F_sub A R P f (` y) (Acc_inv a (proj2_sig y))))
R':=fun x : A =>
forall a : Acc R x, Q x (Fix_F_sub A R P f x a):A -> Type
forall x : A, R' x
    apply (well_founded_induction_type Rwf).A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x : A,
(forall y : {y : A | R y x}, P (` y)) -> P x
Q:forall x : A, P x -> Type
inv:forall x : A,
(forall y : A, R y x -> forall a : Acc R y, Q y (Fix_F_sub A R P f y a)) ->
forall a : Acc R x,
Q x
(f
(fun y : {y : A | R y x} =>
Fix_F_sub A R P f (` y) (Acc_inv a (proj2_sig y))))
R':=fun x : A =>
forall a : Acc R x, Q x (Fix_F_sub A R P f x a):A -> Type
forall x : A, (forall y : A, R y x -> R' y) -> R' x
    subst R'.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x : A,
(forall y : {y : A | R y x}, P (` y)) -> P x
Q:forall x : A, P x -> Type
inv:forall x : A,
(forall y : A, R y x -> forall a : Acc R y, Q y (Fix_F_sub A R P f y a)) ->
forall a : Acc R x,
Q x
(f
(fun y : {y : A | R y x} =>
Fix_F_sub A R P f (` y) (Acc_inv a (proj2_sig y))))
forall x : A,
(forall y : A,
 R y x ->
 (fun x0 : A =>
  forall a : Acc R x0, Q x0 (Fix_F_sub A R P f x0 a))
   y) ->
(fun x0 : A =>
 forall a : Acc R x0, Q x0 (Fix_F_sub A R P f x0 a)) x
    simpl.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x : A,
(forall y : {y : A | R y x}, P (` y)) -> P x
Q:forall x : A, P x -> Type
inv:forall x : A,
(forall y : A, R y x -> forall a : Acc R y, Q y (Fix_F_sub A R P f y a)) ->
forall a : Acc R x,
Q x
(f
(fun y : {y : A | R y x} =>
Fix_F_sub A R P f (` y) (Acc_inv a (proj2_sig y))))
forall x : A,
(forall y : A,
 R y x ->
 forall a : Acc R y, Q y (Fix_F_sub A R P f y a)) ->
forall a : Acc R x, Q x (Fix_F_sub A R P f x a)
    intros.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
Q:forall x0 : A, P x0 -> Type
inv:forall x0 : A,
(forall y : A, R y x0 -> forall a0 : Acc R y, Q y (Fix_F_sub A R P f y a0)) ->
forall a0 : Acc R x0,
Q x0
(f
(fun y : {y : A | R y x0} =>
Fix_F_sub A R P f (` y) (Acc_inv a0 (proj2_sig y))))
x:A
X:forall y : A,
R y x ->
forall a0 : Acc R y, Q y (Fix_F_sub A R P f y a0)
a:Acc R x
Q x (Fix_F_sub A R P f x a)
    rewrite F_unfold...
  Qed.

  (* Let's call f's second parameter its "lowers" function, since it
  provides it access to results for inputs with a lower measure.

  In preparation of lemma similar to Fix_F_sub_rect, but
  for Fix_sub, we first
  need an extra hypothesis stating that the function body has the
  same result for different "lowers" functions (g and h below) as long
  as those produce the same results for lower inputs, regardless
  of the lt proofs. *)

  Hypothesis equiv_lowers:
    forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)),
    (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist (*FIXME shouldn't be needed *) (fun y => R y x0) x p')) ->
      f g = f h.

  (* From equiv_lowers, it follows that
   [Fix_F_sub A R P f x] applications do not not
  depend on the Acc proofs. *)

  Lemma eq_Fix_F_sub x (a a': Acc R x):
    Fix_F_sub A R P f x a =
    Fix_F_sub A R P f x a'.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
equiv_lowers:forall (x0 : A)
  (g
   h : forall x1 : {y : A | R y x0},
       P (` x1)),
(forall (x1 : A) (p p' : R x1 x0),
 g (exist (fun y : A => R y x0) x1 p) =
 h (exist (fun y : A => R y x0) x1 p')) ->
f g = f h
x:A
a, a':Acc R x
Fix_F_sub A R P f x a = Fix_F_sub A R P f x a'
  Proof.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
equiv_lowers:forall (x0 : A)
  (g
   h : forall x1 : {y : A | R y x0},
       P (` x1)),
(forall (x1 : A) (p p' : R x1 x0),
 g (exist (fun y : A => R y x0) x1 p) =
 h (exist (fun y : A => R y x0) x1 p')) ->
f g = f h
x:A
a, a':Acc R x
Fix_F_sub A R P f x a = Fix_F_sub A R P f x a'
    revert a'.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
equiv_lowers:forall (x0 : A)
  (g
   h : forall x1 : {y : A | R y x0},
       P (` x1)),
(forall (x1 : A) (p p' : R x1 x0),
 g (exist (fun y : A => R y x0) x1 p) =
 h (exist (fun y : A => R y x0) x1 p')) ->
f g = f h
x:A
a:Acc R x
forall a' : Acc R x,
Fix_F_sub A R P f x a = Fix_F_sub A R P f x a'
    pattern x, (Fix_F_sub A R P f x a).A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
equiv_lowers:forall (x0 : A)
  (g
   h : forall x1 : {y : A | R y x0},
       P (` x1)),
(forall (x1 : A) (p p' : R x1 x0),
 g (exist (fun y : A => R y x0) x1 p) =
 h (exist (fun y : A => R y x0) x1 p')) ->
f g = f h
x:A
a:Acc R x
(fun (a0 : A) (p : P a0) =>
 forall a' : Acc R a0, p = Fix_F_sub A R P f a0 a') x
  (Fix_F_sub A R P f x a)
    apply Fix_F_sub_rect.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
equiv_lowers:forall (x0 : A)
  (g
   h : forall x1 : {y : A | R y x0},
       P (` x1)),
(forall (x1 : A) (p p' : R x1 x0),
 g (exist (fun y : A => R y x0) x1 p) =
 h (exist (fun y : A => R y x0) x1 p')) ->
f g = f h
x:A
a:Acc R x
forall x0 : A,
(forall y : A,
 R y x0 ->
 forall a0 a' : Acc R y,
 Fix_F_sub A R P f y a0 = Fix_F_sub A R P f y a') ->
forall a0 a' : Acc R x0,
f
  (fun y : {y : A | R y x0} =>
   Fix_F_sub A R P f (` y) (Acc_inv a0 (proj2_sig y))) =
Fix_F_sub A R P f x0 a'
    intros.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
equiv_lowers:forall (x1 : A)
  (g
   h : forall x2 : {y : A | R y x1},
       P (` x2)),
(forall (x2 : A) (p p' : R x2 x1),
 g (exist (fun y : A => R y x1) x2 p) =
 h (exist (fun y : A => R y x1) x2 p')) ->
f g = f h
x:A
a:Acc R x
x0:A
H:forall y : A,
R y x0 ->
forall a1 a'0 : Acc R y,
Fix_F_sub A R P f y a1 = Fix_F_sub A R P f y a'0
a0, a':Acc R x0
f
  (fun y : {y : A | R y x0} =>
   Fix_F_sub A R P f (` y) (Acc_inv a0 (proj2_sig y))) =
Fix_F_sub A R P f x0 a'
    rewrite F_unfold.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
equiv_lowers:forall (x1 : A)
  (g
   h : forall x2 : {y : A | R y x1},
       P (` x2)),
(forall (x2 : A) (p p' : R x2 x1),
 g (exist (fun y : A => R y x1) x2 p) =
 h (exist (fun y : A => R y x1) x2 p')) ->
f g = f h
x:A
a:Acc R x
x0:A
H:forall y : A,
R y x0 ->
forall a1 a'0 : Acc R y,
Fix_F_sub A R P f y a1 = Fix_F_sub A R P f y a'0
a0, a':Acc R x0
f
  (fun y : {y : A | R y x0} =>
   Fix_F_sub A R P f (` y) (Acc_inv a0 (proj2_sig y))) =
f
  (fun y : {y : A | R y x0} =>
   Fix_F_sub A R P f (` y) (Acc_inv a' (proj2_sig y)))
    apply equiv_lowers.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
equiv_lowers:forall (x1 : A)
  (g
   h : forall x2 : {y : A | R y x1},
       P (` x2)),
(forall (x2 : A) (p p' : R x2 x1),
 g (exist (fun y : A => R y x1) x2 p) =
 h (exist (fun y : A => R y x1) x2 p')) ->
f g = f h
x:A
a:Acc R x
x0:A
H:forall y : A,
R y x0 ->
forall a1 a'0 : Acc R y,
Fix_F_sub A R P f y a1 = Fix_F_sub A R P f y a'0
a0, a':Acc R x0
forall (x1 : A) (p p' : R x1 x0),
Fix_F_sub A R P f
  (` (exist (fun y : A => R y x0) x1 p))
  (Acc_inv a0
     (proj2_sig (exist (fun y : A => R y x0) x1 p))) =
Fix_F_sub A R P f
  (` (exist (fun y : A => R y x0) x1 p'))
  (Acc_inv a'
     (proj2_sig (exist (fun y : A => R y x0) x1 p')))
    intros.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x2 : A,
(forall y : {y : A | R y x2}, P (` y)) -> P x2
equiv_lowers:forall (x2 : A)
  (g
   h : forall x3 : {y : A | R y x2},
       P (` x3)),
(forall (x3 : A) (p0 p'0 : R x3 x2),
 g (exist (fun y : A => R y x2) x3 p0) =
 h (exist (fun y : A => R y x2) x3 p'0)) ->
f g = f h
x:A
a:Acc R x
x0:A
H:forall y : A,
R y x0 ->
forall a1 a'0 : Acc R y,
Fix_F_sub A R P f y a1 = Fix_F_sub A R P f y a'0
a0, a':Acc R x0
x1:A
p, p':R x1 x0
Fix_F_sub A R P f
  (` (exist (fun y : A => R y x0) x1 p))
  (Acc_inv a0
     (proj2_sig (exist (fun y : A => R y x0) x1 p))) =
Fix_F_sub A R P f
  (` (exist (fun y : A => R y x0) x1 p'))
  (Acc_inv a'
     (proj2_sig (exist (fun y : A => R y x0) x1 p')))
    apply H.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x2 : A,
(forall y : {y : A | R y x2}, P (` y)) -> P x2
equiv_lowers:forall (x2 : A)
  (g
   h : forall x3 : {y : A | R y x2},
       P (` x3)),
(forall (x3 : A) (p0 p'0 : R x3 x2),
 g (exist (fun y : A => R y x2) x3 p0) =
 h (exist (fun y : A => R y x2) x3 p'0)) ->
f g = f h
x:A
a:Acc R x
x0:A
H:forall y : A,
R y x0 ->
forall a1 a'0 : Acc R y,
Fix_F_sub A R P f y a1 = Fix_F_sub A R P f y a'0
a0, a':Acc R x0
x1:A
p, p':R x1 x0
R (` (exist (fun y : A => R y x0) x1 p')) x0
    assumption.
  Qed.

  (* Finally, Fix_F_rect lets one prove a property of
  functions defined using Fix_F_sub by showing that
  property to be invariant over single application of the function
  body (f). *)

  Lemma Fix_sub_rect
    (Q: forall x, P x -> Type)
    (inv: forall
      (x: A)
      (H: forall (y: A), R y x -> Q y (Fix_sub A R Rwf P f y))
      (a: Acc R x),
        Q x (f (fun y: {y: A | R y x} => Fix_sub A R Rwf P f (proj1_sig y))))
    : forall x, Q _ (Fix_sub A R Rwf P f x).A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x : A,
(forall y : {y : A | R y x}, P (` y)) -> P x
equiv_lowers:forall (x0 : A)
  (g
   h : forall x : {y : A | R y x0},
       P (` x)),
(forall (x : A) (p p' : R x x0),
 g (exist (fun y : A => R y x0) x p) =
 h (exist (fun y : A => R y x0) x p')) ->
f g = f h
Q:forall x : A, P x -> Type
inv:forall x : A,
(forall y : A,
 R y x -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x ->
Q x
  (f
     (fun y : {y : A | R y x} =>
      Fix_sub A R Rwf P f (` y)))
forall x : A, Q x (Fix_sub A R Rwf P f x)
  Proof with auto.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x : A,
(forall y : {y : A | R y x}, P (` y)) -> P x
equiv_lowers:forall (x0 : A)
  (g
   h : forall x : {y : A | R y x0},
       P (` x)),
(forall (x : A) (p p' : R x x0),
 g (exist (fun y : A => R y x0) x p) =
 h (exist (fun y : A => R y x0) x p')) ->
f g = f h
Q:forall x : A, P x -> Type
inv:forall x : A,
(forall y : A,
 R y x -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x ->
Q x
  (f
     (fun y : {y : A | R y x} =>
      Fix_sub A R Rwf P f (` y)))
forall x : A, Q x (Fix_sub A R Rwf P f x)
    unfold Fix_sub.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x : A,
(forall y : {y : A | R y x}, P (` y)) -> P x
equiv_lowers:forall (x0 : A)
  (g
   h : forall x : {y : A | R y x0},
       P (` x)),
(forall (x : A) (p p' : R x x0),
 g (exist (fun y : A => R y x0) x p) =
 h (exist (fun y : A => R y x0) x p')) ->
f g = f h
Q:forall x : A, P x -> Type
inv:forall x : A,
(forall y : A,
 R y x -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x ->
Q x
  (f
     (fun y : {y : A | R y x} =>
      Fix_sub A R Rwf P f (` y)))
forall x : A, Q x (Fix_F_sub A R P f x (Rwf x))
    intros.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
equiv_lowers:forall (x0 : A)
  (g
   h : forall x1 : {y : A | R y x0},
       P (` x1)),
(forall (x1 : A) (p p' : R x1 x0),
 g (exist (fun y : A => R y x0) x1 p) =
 h (exist (fun y : A => R y x0) x1 p')) ->
f g = f h
Q:forall x0 : A, P x0 -> Type
inv:forall x0 : A,
(forall y : A,
 R y x0 -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x0 ->
Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_sub A R Rwf P f (` y)))
x:A
Q x (Fix_F_sub A R P f x (Rwf x))
    apply Fix_F_sub_rect.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
equiv_lowers:forall (x0 : A)
  (g
   h : forall x1 : {y : A | R y x0},
       P (` x1)),
(forall (x1 : A) (p p' : R x1 x0),
 g (exist (fun y : A => R y x0) x1 p) =
 h (exist (fun y : A => R y x0) x1 p')) ->
f g = f h
Q:forall x0 : A, P x0 -> Type
inv:forall x0 : A,
(forall y : A,
 R y x0 -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x0 ->
Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_sub A R Rwf P f (` y)))
x:A
forall x0 : A,
(forall y : A,
 R y x0 ->
 forall a : Acc R y, Q y (Fix_F_sub A R P f y a)) ->
forall a : Acc R x0,
Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_F_sub A R P f (` y)
        (Acc_inv a (proj2_sig y))))
    intros.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
equiv_lowers:forall (x1 : A)
  (g
   h : forall x2 : {y : A | R y x1},
       P (` x2)),
(forall (x2 : A) (p p' : R x2 x1),
 g (exist (fun y : A => R y x1) x2 p) =
 h (exist (fun y : A => R y x1) x2 p')) ->
f g = f h
Q:forall x1 : A, P x1 -> Type
inv:forall x1 : A,
(forall y : A,
 R y x1 -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x1 ->
Q x1
  (f
     (fun y : {y : A | R y x1} =>
      Fix_sub A R Rwf P f (` y)))
x, x0:A
X:forall y : A,
R y x0 ->
forall a0 : Acc R y, Q y (Fix_F_sub A R P f y a0)
a:Acc R x0
Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_F_sub A R P f (` y)
        (Acc_inv a (proj2_sig y))))
    assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y)))...A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
equiv_lowers:forall (x1 : A)
  (g
   h : forall x2 : {y : A | R y x1},
       P (` x2)),
(forall (x2 : A) (p p' : R x2 x1),
 g (exist (fun y : A => R y x1) x2 p) =
 h (exist (fun y : A => R y x1) x2 p')) ->
f g = f h
Q:forall x1 : A, P x1 -> Type
inv:forall x1 : A,
(forall y : A,
 R y x1 -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x1 ->
Q x1
  (f
     (fun y : {y : A | R y x1} =>
      Fix_sub A R Rwf P f (` y)))
x, x0:A
X:forall y : A,
R y x0 ->
forall a0 : Acc R y, Q y (Fix_F_sub A R P f y a0)
a:Acc R x0
X0:forall y : A,
R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))
Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_F_sub A R P f (` y)
        (Acc_inv a (proj2_sig y))))
    set (inv x0 X0 a).A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
equiv_lowers:forall (x1 : A)
  (g
   h : forall x2 : {y : A | R y x1},
       P (` x2)),
(forall (x2 : A) (p p' : R x2 x1),
 g (exist (fun y : A => R y x1) x2 p) =
 h (exist (fun y : A => R y x1) x2 p')) ->
f g = f h
Q:forall x1 : A, P x1 -> Type
inv:forall x1 : A,
(forall y : A,
 R y x1 -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x1 ->
Q x1
  (f
     (fun y : {y : A | R y x1} =>
      Fix_sub A R Rwf P f (` y)))
x, x0:A
X:forall y : A,
R y x0 ->
forall a0 : Acc R y, Q y (Fix_F_sub A R P f y a0)
a:Acc R x0
X0:forall y : A,
R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))
q:=inv x0 X0 a:Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_sub A R Rwf P f (` y)))
Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_F_sub A R P f (` y)
        (Acc_inv a (proj2_sig y)))) clearbody q.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
equiv_lowers:forall (x1 : A)
  (g
   h : forall x2 : {y : A | R y x1},
       P (` x2)),
(forall (x2 : A) (p p' : R x2 x1),
 g (exist (fun y : A => R y x1) x2 p) =
 h (exist (fun y : A => R y x1) x2 p')) ->
f g = f h
Q:forall x1 : A, P x1 -> Type
inv:forall x1 : A,
(forall y : A,
 R y x1 -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x1 ->
Q x1
  (f
     (fun y : {y : A | R y x1} =>
      Fix_sub A R Rwf P f (` y)))
x, x0:A
X:forall y : A,
R y x0 ->
forall a0 : Acc R y, Q y (Fix_F_sub A R P f y a0)
a:Acc R x0
X0:forall y : A,
R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))
q:Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_sub A R Rwf P f (` y)))
Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_F_sub A R P f (` y)
        (Acc_inv a (proj2_sig y))))
    rewrite <- (equiv_lowers (fun y: {y: A | R y x0} =>
      Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y)))
    (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))...A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
equiv_lowers:forall (x1 : A)
  (g
   h : forall x2 : {y : A | R y x1},
       P (` x2)),
(forall (x2 : A) (p p' : R x2 x1),
 g (exist (fun y : A => R y x1) x2 p) =
 h (exist (fun y : A => R y x1) x2 p')) ->
f g = f h
Q:forall x1 : A, P x1 -> Type
inv:forall x1 : A,
(forall y : A,
 R y x1 -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x1 ->
Q x1
  (f
     (fun y : {y : A | R y x1} =>
      Fix_sub A R Rwf P f (` y)))
x, x0:A
X:forall y : A,
R y x0 ->
forall a0 : Acc R y, Q y (Fix_F_sub A R P f y a0)
a:Acc R x0
X0:forall y : A,
R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))
q:Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_sub A R Rwf P f (` y)))
forall (x1 : A) (p p' : R x1 x0),
Fix_F_sub A R P f
  (` (exist (fun y : A => R y x0) x1 p))
  (Rwf (` (exist (fun y : A => R y x0) x1 p))) =
Fix_F_sub A R P f
  (` (exist (fun y : A => R y x0) x1 p'))
  (Acc_inv a
     (proj2_sig (exist (fun y : A => R y x0) x1 p')))
    intros.A:Type
P:A -> Type
R:A -> A -> Prop
Rwf:well_founded R
f:forall x2 : A,
(forall y : {y : A | R y x2}, P (` y)) -> P x2
equiv_lowers:forall (x2 : A)
  (g
   h : forall x3 : {y : A | R y x2},
       P (` x3)),
(forall (x3 : A) (p0 p'0 : R x3 x2),
 g (exist (fun y : A => R y x2) x3 p0) =
 h (exist (fun y : A => R y x2) x3 p'0)) ->
f g = f h
Q:forall x2 : A, P x2 -> Type
inv:forall x2 : A,
(forall y : A,
 R y x2 -> Q y (Fix_sub A R Rwf P f y)) ->
Acc R x2 ->
Q x2
  (f
     (fun y : {y : A | R y x2} =>
      Fix_sub A R Rwf P f (` y)))
x, x0:A
X:forall y : A,
R y x0 ->
forall a0 : Acc R y, Q y (Fix_F_sub A R P f y a0)
a:Acc R x0
X0:forall y : A,
R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))
q:Q x0
  (f
     (fun y : {y : A | R y x0} =>
      Fix_sub A R Rwf P f (` y)))
x1:A
p, p':R x1 x0
Fix_F_sub A R P f
  (` (exist (fun y : A => R y x0) x1 p))
  (Rwf (` (exist (fun y : A => R y x0) x1 p))) =
Fix_F_sub A R P f
  (` (exist (fun y : A => R y x0) x1 p'))
  (Acc_inv a
     (proj2_sig (exist (fun y : A => R y x0) x1 p')))
    apply eq_Fix_F_sub.
  Qed.

End Fix_rects.

Tactic to fold a definition based on Fix_measure_sub.

Ltac fold_sub f :=
  match goal with
    | [ |- ?T ] =>
      match T with
        context C [ @Fix_sub _ _ _ _ _ ?arg ] =>
        let app := context C [ f arg ] in
          change app
      end
  end.

This module provides the fixpoint equation provided one assumes functional extensionality.

Module WfExtensionality.

The two following lemmas allow to unfold a well-founded fixpoint definition without restriction using the functional extensionality axiom.

For a function defined with Program using a well-founded order.

  Lemma fix_sub_eq_ext :
    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 (` 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 (` y)).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 (` y)) ->
           P x) (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 (` y))
  Proof.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 (` y)) ->
           P x) (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 (` y))
    intros ; apply Fix_eq ; auto.A:Type
R:A -> A -> Prop
Rwf:well_founded R
P:A -> Type
F_sub:forall x0 : A,
(forall y : {y : A | R y x0}, P (` y)) -> P x0
x:A
forall (x0 : A)
  (f g : forall y : {y : A | R y x0}, P (` y)),
(forall y : {y : A | R y x0}, f y = g y) ->
F_sub x0 f = F_sub x0 g
    intros.A:Type
R:A -> A -> Prop
Rwf:well_founded R
P:A -> Type
F_sub:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
x, x0:A
f, g:forall y : {y : A | R y x0}, P (` y)
H:forall y : {y : A | R y x0}, f y = g y
F_sub x0 f = F_sub x0 g
    assert(f = g).A:Type
R:A -> A -> Prop
Rwf:well_founded R
P:A -> Type
F_sub:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
x, x0:A
f, g:forall y : {y : A | R y x0}, P (` y)
H:forall y : {y : A | R y x0}, f y = g y
f = g
A:Type
R:A -> A -> Prop
Rwf:well_founded R
P:A -> Type
F_sub:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
x, x0:A
f, g:forall y : {y : A | R y x0}, P (` y)
H:forall y : {y : A | R y x0}, f y = g y
H0:f = g
F_sub x0 f = F_sub x0 g
    -A:Type
R:A -> A -> Prop
Rwf:well_founded R
P:A -> Type
F_sub:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
x, x0:A
f, g:forall y : {y : A | R y x0}, P (` y)
H:forall y : {y : A | R y x0}, f y = g y
f = g extensionality y ; apply H.
    -A:Type
R:A -> A -> Prop
Rwf:well_founded R
P:A -> Type
F_sub:forall x1 : A,
(forall y : {y : A | R y x1}, P (` y)) -> P x1
x, x0:A
f, g:forall y : {y : A | R y x0}, P (` y)
H:forall y : {y : A | R y x0}, f y = g y
H0:f = g
F_sub x0 f = F_sub x0 g rewrite H0 ; auto.
  Qed.

Tactic to unfold once a definition based on Fix_sub.

  Ltac unfold_sub f fargs :=
    set (call:=fargs) ; unfold f in call ; unfold call ; clear call ;
      rewrite fix_sub_eq_ext ; repeat fold_sub f ; simpl proj1_sig.

End WfExtensionality.