Goal:
    G : t  s0 : VSet.t  x : V.t  s1 : VSet.t  x0 : V.t
  ============================
   (noConfusion_SPath_obligation_2
      {|
        pr1 := {| pr1 := s0; pr2 := {| pr1 := x; pr2 := x |} |};
        pr2 := spath_refl s0 x
      |}
      {|
        pr1 :=
          {|
            pr1 := pr1 {| pr1 := s0; pr2 := x |};
            pr2 :=
              {|
                pr1 := pr2 {| pr1 := s0; pr2 := x |};
                pr2 := pr2 {| pr1 := s0; pr2 := x |}
              |}
          |};
        pr2 :=
          spath_refl (pr1 {| pr1 := s0; pr2 := x |})
            (pr2 {| pr1 := s0; pr2 := x |})
      |}
      (noConfusion_SPath_obligation_1
         {|
           pr1 := {| pr1 := s0; pr2 := {| pr1 := x; pr2 := x |} |};
           pr2 := spath_refl s0 x
         |}
         {|
           pr1 :=
             {|
               pr1 := pr1 {| pr1 := s0; pr2 := x |};
               pr2 :=
                 {|
                   pr1 := pr2 {| pr1 := s0; pr2 := x |};
                   pr2 := pr2 {| pr1 := s0; pr2 := x |}
                 |}
             |};
           pr2 :=
             spath_refl (pr1 {| pr1 := s0; pr2 := x |})
               (pr2 {| pr1 := s0; pr2 := x |})
         |} eq_refl) = eq_refl)


DEBUG:Going to execute:
simpl