Set Implicit Arguments.

Section Acc_irrelevance.

  Variable (X : Type) (R : X -> X -> Prop).


  Inductive Acc_eq : forall x, Acc R x -> Acc R x -> Prop :=
    | in_Acc_eq : forall x A1 A2, (forall y H, @Acc_eq y (A1 y H) (A2 y H))
                               -> @Acc_eq x (Acc_intro _ A1) (Acc_intro _ A2).


  Fact Acc_eq_total x H1 H2 : @Acc_eq x H1 H2.
  Proof.
    revert H2.
    induction H1 as [ ? ? IH ] using Acc_inv_dep.
    intros []; constructor; intros; apply IH.
  Qed.


  Variables (P : X -> Type) (f : forall x, Acc R x -> P x)
            (Hf : forall x H1 H2, (forall y Hy, f (H1 y Hy) = f (H2 _ Hy))
                               -> f (Acc_intro x H1) = f (Acc_intro x H2)).

  Theorem Acc_irrelevance x H1 H2 : @f x H1 = f H2.
  Proof.
    generalize (Acc_eq_total H1 H2).
    induction 1 as [ x H1 H2 _ IH ].
    apply Hf, IH.
  Qed.

End Acc_irrelevance.