Stackoverflow.v

Section T. 
  
  Variables (A : Type) (B : A -> Type).

  Inductive W : Type := suc : forall (a : A), (B a -> W) -> W.

  Variables (P : W -> Type).
  Fixpoint rec (H : forall a f, (forall b, P (f b)) -> P (suc a f)) (x : W) : P x
    := match x with suc a f => H a f (fun b => rec H (f b)) end.

    
  Fixpoint rec2 (H : forall (a : A) (f : B a -> W) 
    (IH : forall b : B a, P (f b)),
    (forall b1 b2 : B a, f b1 = f b2 -> existT P (f b1) (IH b1) = existT P (f b2) (IH b2)) -> P (suc a f))
    (x : W) {struct x} : P x.
  Proof.
    refine 
    (match x with
    | suc a f =>
        H a f
          (fun b : B a => rec2 H (f b)) (* This one looks fishy to me. *)
          (fun (b1 b2 : B a) (eqp : f b1 = f b2) =>
          eq_existT_curried eqp (f_equal_dep P (rec2 H) eqp))
    end). 
    Fail Guarded.