Goal:
    G : t
  ============================
   (forall
      (a
       b : sigma
             (fun
                index : sigma (fun _ : VSet.t => sigma (fun _ : V.t => V.t))
              => SPath (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index))))
      (e : NoConfusion_SPath a b),
    (fun
       (a0
        b0 : sigma
               (fun
                  index : sigma
                            (fun _ : VSet.t => sigma (fun _ : V.t => V.t)) =>
                SPath (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index))))
       (H : a0 = b0) => noConfusion_SPath_obligation_2 a0 b0 H) a b
      ((fun
          (a0
           b0 : sigma
                  (fun
                     index : sigma
                               (fun _ : VSet.t => sigma (fun _ : V.t => V.t))
                   => SPath (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index))))
          (H : NoConfusion_SPath a0 b0) =>
        noConfusion_SPath_obligation_1 a0 b0 H) a b e) = e)


DEBUG:Going to execute:
simpl; intros;
            match goal with
            | H:_ = _ |- _ = _ => try solve_noconf_inv_equiv
            | H:_ = _ |- _ => try solve_noconf_prf
            | |- _ = _ => try solve_noconf_inv
            end