Tw.v

Section Wf.

  Variables 
    (A : Type)
    (R : A -> A -> Prop).

  Inductive Acc (x: A) : Prop :=
    Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.

  Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
  Proof.
    destruct 1; 
    trivial.
  Defined.

  (* 
  Context 
    (x : A)
    (h : Acc x).
  Check Acc_intro _ (fun (y : A) (hy : R y x) =>
    Acc_inv x h y hy).
  *)

End Wf.


Section Fxpoint.

  
  Variables 
    (A : Type)
    (R : A -> A -> Prop)
    (P : A -> Type)
    (F : forall (x : A), (forall (y : A), R y x -> P y) -> P x).

  
  Fixpoint Fix_F (x : A) (a : Acc A R x) : P x :=
    F x (fun (y : A) (hy : R y x) => 
      Fix_F y (Acc_inv A R x a y hy)).

  Scheme Acc_inv_dep := Induction for Acc Sort Prop.

  Lemma Fix_F_eq (x : A) (a : Acc A R x) :
     F x 
     (fun (y:A) (hy : R y x) => 
      Fix_F y (Acc_inv A R x a y hy )) = 
    Fix_F x a.
  Proof.
   destruct a using Acc_inv_dep; auto.
  Qed.